Interactive theorem provers [1]}, [2]}, [3]} already checked proofs of consensus algorithms used in the blockchain industry.
In particular, Coq helped prove the Raft consensus algorithm [4]}, which is not Byzantine fault tolerant but part of crash fault tolerant distributed ledgers [5]}, [6]}, and the Byzantine consensus algorithm of the Algorand blockchain [7]}.
In addition, Dafny [8]} proved MultiPaxos, a consensus algorithm that tolerates crash failures.
Isabelle/HOL [9]} was used to prove Byzantine fault tolerant algorithms [10]} and was combined with Ivy to try to prove the Byzantine consensus protocol of the Stellar blockchain [11]} as discussed in the introduction.
Theorem provers check proofs, not the algorithms.
Hence, one has to invest efforts into writing detailed mechanical proofs.
