Awesome

LibraChain

A library providing mechanized proofs of the LibraBFT consensus using the Coq theorem prover.

Architecture & Evolution

This library uses the SSreflect proof language and mathematical components libraries for Coq.

It is compatible with, inspired by, and extends, the ToyChain library by George Pirlea, Ilya Sergey et al.

This library is at an experimental stage and its contents may know significant evolutions in the future.

References

Libra Technical Papers

• The Libra Blockchain
• State Machine Replication in the Libra Blockchain

HotStuff technical Papers

LibraBFT, studied here, is a Hotstuff-inspired protocol.

• PODC paper
• ArXiV full version

Versions of the Libra Consensus Papers

Due to the high level of precision requires for a formalized proof, consultation of both LibraBFT v2 & v3 is recommended:

• LibraBFT v2
• LibraBFT v3

Coq libraries used in this development

• SSReflect
• ToyChain master's thesis of George Pirlea
• Mechanizing BlockChain consensus

Contributing

See the CONTRIBUTING file for how to help out.

LICENSE

LibraChain is Apache-2.0 licensed, as found in the LICENSE file.