[ziedaniel1]

If anyone's interested in proving distributed algorithms correct, they should check out the Verdi project (https://github.com/uwplse/verdi), which has proved Raft correct in Coq. I imagine handling Byzantine faults and the full complexity of SCP would be quite a bit harder, but probably doable.

To me, though, it would be more interesting to prove the implementation correct. Rather than trying to prove an existing C++ implementation correct, it's probably more feasible to reimplement the algorithm within Coq and extract to runnable code. Verdi already supports that, but unfortunately it doesn't support disk state.