The Algorand consensus protocol is the foundation of a decentralized digital currency and transactions platform. This project provides a model of the protocol in Coq, expressed as a transition system over global states in a message-passing distributed system. Included is a formal proof of safety for the transition system.
- License: University of Illinois/NCSA Open Source License
- Compatible Coq versions: 8.12
- Additional dependencies:
- Coq namespace:
- Related publication(s):
We recommend installing the dependencies of the project via OPAM, for example:
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-algebra coq-mathcomp-finmap.1.5.0 \ coq-mathcomp-analysis.0.3.2 coq-record-update
make in the project root directory. This will check all the definitions and proofs.
The project includes:
- an abstract and timed specification in Coq of the Algorand consensus protocol as a transition system, including node-level behavior, asynchronous messaging and a model of the adversary,
- a complete formal proof of asynchronous safety for the transition system.
For more details on the formalization, see the report:
Statements of some liveness properties for the transition system are also provided, but these are work-in-progress and their proofs are currently incomplete.
All Coq source files can be found under the
theories directory, and their content is as follows:
zify.v: definitions for using the
liaarithmetic tactic for MathComp from mczify
fmap_ext.v: auxiliary definitions and results on finite maps
algorand_model.v: definition of the Algorand local state, global state, and transition system, along with helper functions and facts
safety_helpers.v: helper functions and lemmas used when proving safety of the transition system
quorums.v: definitions and hypotheses about quorums of nodes
safety.v: statement and complete formal proof of safety for the transition system
liveness.v: an initial attempt at specifying liveness properties for the transition system. This part is work-in-progress and thus the file contains incomplete (admitted) proofs.
Help and Feedback
Feel free to report GitHub issues or to contact us at: firstname.lastname@example.org