CKB Verification

A formal model of CKB consensus protocol in Coq and proof of quiescent consistency property.

Requirements

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.

Name		Name	Last commit message	Last commit date
Latest commit History 3 Commits
Properties		Properties
Structures		Structures
Systems		Systems
.gitattributes		.gitattributes
.gitignore		.gitignore
LICENSE		LICENSE
Makefile		Makefile
README.md		README.md
_CoqProject		_CoqProject