Take a look here for pointers to formal proofs: https://news.ycombinator.com/item?id=10017549 https://news.ycombinator.com/item?id=10017549 Specifically Verdi

Take a look here for pointers to formal proofs: https://news.ycombinator.com/item?id=10017549 https://news.ycombinator.com/item?id=10017549 Specifically Verdi, a Coq framework for distributed system verification, which now includes a formally proven Raft implementation. https://github.com/uwplse/verdi https://github.com/uwplse/verdi This appears to be the main theorem, "raft_linearizable": https://github.com/uwplse/verdi/blob/master/raft-proofs/EndToEndLinearizability.v https://github.com/uwplse/verdi/blob/master/raft-proofs/EndT...