Which mechanized proofs for the consensus?

Consensus
#1

Hello,

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.

Thanks,

1 Like
#2

We would like to use tools such as Coq to verify the formal proofs specified in https://developers.libra.org/docs/state-machine-replication-paper. We have begun early prototyping in this space, but do not have an estimate of when we will complete this work.

3 Likes
#3

Great, thank you for the answer!
I look forward to seeing this work

1 Like
#5

We have completed a Coq proof of the safety property of the LibraBFT Consensus.

The proof was recently open-sourced, and its code can be accessed and checked here:

A talk was given at the TPBC’20 workshop on this effort:

–
FG

2 Likes