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