A minimalistic blockchain consensus implemented and verified in Coq
Switch branches/tags
Nothing to show
Clone or download



Build Status

A Coq implementation of a minimalistic blockchain-based consensus protocol.

Building the Project



We recommend installing the requirements via OPAM:

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-mathcomp-ssreflect coq-fcsl-pcm

Then, run make clean; make from the root folder. This will build all the libraries and check all the proofs.

Project Structure

The top-level structure consists of the following folders:

  • Structures - implementations of block forests and chain properties;

  • Systems - definition of the protocol, its state, and network semantics;

  • Properties - proved properties of the protocol, e.g., eventual consistency for a clique-like network topology;

Obsolete development

  • Obsolete -- properties that might or might not hold, as were verified out of many optimistically assumed axioms at the beginning of the project.