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/platform#security.
Articles in this section
- 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?
- How efficient is the hashgraph consensus algorithm?
- Does the FLP theorem say aBFT consensus is impossible?
- Where can I find more information about the hashgraph Coq proof?