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.
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.