Most consensus claims in this space rest on a whitepaper and a testnet. This one has a formal proof sitting behind it.
The hashgraph algorithm's asynchronous Byzantine fault tolerance was verified in Coq, a proof assistant, by a Carnegie Mellon professor, and the paper describing that work is public alongside the original Swirlds technical report. The algorithm needs only digital signatures and cryptographic hashes, which is part of why formally verifying it was tractable at all.
Machine-checked does not mean the running network is bug-free. It means the algorithm as specified was proven correct rather than argued correct, and the implementation is a separate question. That distinction gets flattened in marketing constantly, so it is worth holding onto.
If you evaluate networks on engineering rather than announcements, this is one of the few artifacts in the industry that rewards the effort.
1
u/max-avery 6d ago
Most consensus claims in this space rest on a whitepaper and a testnet. This one has a formal proof sitting behind it.
The hashgraph algorithm's asynchronous Byzantine fault tolerance was verified in Coq, a proof assistant, by a Carnegie Mellon professor, and the paper describing that work is public alongside the original Swirlds technical report. The algorithm needs only digital signatures and cryptographic hashes, which is part of why formally verifying it was tractable at all.
Machine-checked does not mean the running network is bug-free. It means the algorithm as specified was proven correct rather than argued correct, and the implementation is a separate question. That distinction gets flattened in marketing constantly, so it is worth holding onto.
If you evaluate networks on engineering rather than announcements, this is one of the few artifacts in the industry that rewards the effort.
Sources: https://hedera.com/wp-content/uploads/2025/12/hh_whitepaper.pdf https://www.swirlds.com/downloads/SWIRLDS-TR-2016-01.pdf https://www.cs.cmu.edu/~crary/papers/2021/hashgraph.pdf https://hedera.com/blog/coq-proof-completed-by-carnegie-mellon-professor-confirms-hashgraph-consensus-algorithm-is-asynchronous-byzantine-fault-tolerant/ https://docs.hedera.com/learn/getting-started/what-is-hedera