The hashgraph consensus algorithm has been validated as asynchronous Byzantine fault tolerant by a math proof checked by computer using Coq, a formal proof verification system. Coq provides a formal language to write mathematical definitions and executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs. It is often used for certifying the properties of programs, programming languages, and mathematics. The Coq proof of hashgraph was completed by a Carnegie Mellon associate professor of Computer Science. We are not aware of any professors or academics from other institutions who have conducted a Coq analysis of hashgraph, but given the Coq proof is a computer-checked proof (and thus avoids human error) and verified hashgraph as ABFT, we think academics are unlikely to see a reason to verify the proof again. The formalized proof is available at: https://www.hedera.com/hashgraph-coq.zip
- Categories
Articles in this section
- What are the material financial terms of the license agreement between Hedera and Swirlds?
- Can Hedera’s license to use the hashgraph technology be revoked? If so, in what situations?
- Does Hedera have an exclusive license to use the hashgraph technology?
- How much bandwidth overhead does gossip about gossip add to messages?
- Have any non-Carnegie Mellon professors or academics verified hashgraph as asynchronous Byzantine fault tolerant (ABFT)?
- Who generates the timestamp on a transaction?
- What is 'gossip about gossip and 'virtual voting'?
- Why was hashgraph invented?
- Is the hashgraph consensus algorithm patented?
- How can hashgraph deliver consensus without proof-of-work?