[yodsanklai]

Are they talking about computer verified proofs? I wonder, are researchers able to prove the correctness of distributed algorithms the same way they would prove sequential algorithms (for instance, using some type of Hoare logic and sat solver/ proof assistant).

[djb_hackernews]

You may be interested in this[0] paper outlining AWS use of TLA+ to formally prove its systems. Also previous discussion here[1].

[0] http://research.microsoft.com/en-us/um/people/lamport/tla/fo...

[1] https://news.ycombinator.com/item?id=8096185

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

[mazieres]

No. At least for the moment, the proofs are English language only.