Algorand Verification

About

Welcome to the Algorand Verification project website!

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.

This is an open source project, licensed under the University of Illinois/NCSA Open Source License.

Get the code

The latest release of Algorand Verification can be downloaded from GitHub.

Documentation

Generated HTML documentation is available for source files in the latest release:

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

Help and contact

Report issues on GitHub

Authors

Musab A. Alturki
Jing Chen
Victor Luchangco
Brandon Moore
Karl Palmskog
Lucas Peña
Grigore Roșu