Comment by pavpanchekha

To add on to wilcoxjay's excellent response, this sort of proof development is exactly what Voevodsky would like to (eventually) see happen in mathematics. The linked proof of Raft uses Coq, which is a small proof checker which makes sure that no mistakes were made in the proof. Simpler, "paper" proofs had already been done for Raft.