A library providing mechanized proofs of the LibraBFT consensus using the Coq theorem prover.
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.
LibraBFT, studied here, is a Hotstuff-inspired protocol.
Due to the high level of precision requires for a formalized proof, consultation of both LibraBFT v2 & v3 is recommended:
See the CONTRIBUTING file for how to help out.
LibraChain is Apache-2.0 licensed, as found in the LICENSE file.