A formal model of CKB consensus protocol in Coq and proof of quiescent consistency property.
We recommend installing the Coq requirements via OPAM:
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq.8.12.0 coq-mathcomp-ssreflect.1.11.0 coq-mathcomp-finmap.1.5.0
Then run make in the project root directory, this will check all the definitions and proofs.