Would you consider TLA+ functional? It sounds like the tension you're describing might be how most distributed consensus protocols are implemented as imperative

Would you consider TLA+ functional? It sounds like the tension you're describing might be how most distributed consensus protocols are implemented as imperative code, and part of the Raft excursion involved writing a TLA+ proof of the protocol. https://github.com/ongardie/raft.tla https://github.com/ongardie/raft.tla