# Verifying the Hashgraph Consensus Algorithm

arXiv: https://arxiv.org/abs/2102.01167 · HTML: https://mlsanity.com/paper/2102.01167/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 1 Feb 2021.

## Built on by (most cited first, 2 of 2)

- [Enabling Integration and Interaction for Decentralized Artificial Intelligence in Airline Disruption Management](https://mlsanity.com/paper/2104.03349/) (2021)
- [A Hashgraph-Inspired Consensus Mechanism for Reliable Multi-Model Reasoning](https://mlsanity.com/paper/2505.03553/) (2025)

## Abstract (arXiv)

The Hashgraph consensus algorithm is an algorithm for asynchronous Byzantine fault tolerance intended for distributed shared ledgers. Its main distinguishing characteristic is it achieves consensus without exchanging any extra messages; each participant's votes can be determined from public information, so votes need not be transmitted. In this paper, we discuss our experience formalizing the Hashgraph algorithm and its correctness proof using the Rocq proof assistant. The paper is self-contained; it includes a complete discussion of the algorithm and its correctness argument in English.
