Correctness proof for the Hashgraph Consensus algorithm, formalized in Coq.

A formalization of The Swirlds Hashgraph Consensus Algorithm: Fair, Fast, Byzantine Fault Tolerance, by Leemon Baird. Formalized in Coq by Karl Crary, using some insights arising from an earlier, partial formalization by Gregory Malecha and Ryan Wisnesky.

Build Instructions

The development is self-contained and should build without modification using Coq version 8.8.0. Just run make.

Theorems

All theorems, lemmas, definitions, and axioms are listed in the codoq index.

Libraries (in dependency order)

Timestamp
Order
Median          Received
Fairness
Famous
Consensus
Decision          Progress
Vote
Round
Sees
HashgraphFacts
Hashgraph
Majority
Calculate          Cardinality
Weight
Decide
Relation
Tact