Algorand Verification

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.

Meta

• License: University of Illinois/NCSA Open Source License
• Compatible Coq versions: 8.12
• Additional dependencies:
  • MathComp ssreflect 1.11.0
  • MathComp algebra
  • MathComp finmap 1.5.0
  • MathComp analysis 0.3.2
  • Coq record update
• Coq namespace: Algorand
• Related publication(s):
  • Towards a Verified Model of the Algorand Consensus Protocol in Coq doi:10.1007/978-3-030-54994-7_27

Building

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

Then, run make in the project root directory. This will check all the definitions and proofs.

Contents

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:

Modeling and Verification of the Algorand Consensus Protocol

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 lia arithmetic 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: [email protected]