In the blog post “Libra: The Path Forward”, some mechanized proofs of the consensus are evoked:
Mechanized proofs — We plan to start using mechanized proofs to verify our tech report and protocol claims.
There is still little work on mechanized proofs of asynchronous consensus algorithms and it can be interesting to know more. Please does someone have any precision on this? Is it just a general orientation or some progress have already been made? For instance a formal specification in something like TLA+, some model checking or a beginning of proof in Coq or Isabelle.