And for anything more or less complex and optimised (e.g. Egalitarian Paxos), you'll not only end up with proving the correctness of the algorithm, but also the correctness of the implementation (which by themselves will hugely vary).

I see way more future in one's ability to write proofs of correctness in the comments before the function definition in any language; rather than preferring any specific language for the sake of proof.