Coq Proof Completed By Carnegie Mellon Professor Confirms… | Hedera Hedera Network Services Token Service Mint and configure tokens and accounts. Consensus Service Verifiable timestamps and ordering of events. Smart Contracts Run Solidity smart contracts. HBAR The Hedera network's native cryptocurrency. Insights How It Works Learn about Hedera from end to end. Explorers View live and historical data on Hedera. Dashboards Analyze network activity and metrics. Network Nodes Understand networks and node types. Devs Start Building Get Started Learn core concepts and build the future. Documentation Review the API and build using your favorite language. Developer Resources Integrations Plugins and microservices for Hedera. Fee Estimator Understand and estimate transaction costs. Open Source Hedera is committed to open, transparent code. Learning Center Learn about web3 and blockchain technologies. Grants Grants & accelerators for your project. Bounties Find bugs. Submit a report. Earn rewards. Ecosystem ECOSYSTEM Hedera Ecosystem Applications, developer tools, network explorers, and more. NFT Ecosystem Metrics Analyze on-chain and market NFT ecosystem metrics. CATEGORIES Web3 Applications Connect into the innovative startups decentralizing the web on Hedera. Enterprise Applications Learn about the Fortune 500 companies decentralizing the web on Hedera. Wallets & Custodians Create a Hedera account to manage HBAR, fungible tokens, and NFTs. Network Explorers Hedera mainnet and testnet graphical network explorers. Developer Tooling Third-party APIs, integrations, and plugins to build apps on Hedera. Grants & Accelerators Boost your project with support from the Hedera ecosystem. Partner Program Explore our partners to bring your vision into reality. Hedera Council Over 30 highly diversified organizations govern Hedera. Use Cases Hedera Solutions Asset Tokenization Studio Open source toolkit for tokenizing assets securely. Stablecoin Studio All-in-one toolkit for stablecoin solutions. Hedera Guardian Auditable carbon markets and traceability. Functional Use Cases Data Integrity & AI Reliable, secure, and ethically governed insights. Sustainability Enabling fair carbon markets with trust. Real-World Asset Tokenization Seamless tokenization of real-world assets and digital at scale. Consumer Engagement & Loyalty Mint, distribute, and redeem loyalty rewards. Decentralized Identity Maintain the lifecycle of credentials. Decentralized Logs Scalable, real-time timestamped events. DeFi Dapps built for the next-generation of finance. NFTs Low, fixed fees. Immutable royalties. Payments Scalable, real-time, and affordable crypto-payments. HBAR Overview Learn about Hedera's token, HBAR. Treasury Management Hedera’s report of the HBAR supply. Governance Decentralized Governance Hedera Council See the world's leading organizations that own Hedera. About Meet Hedera's Board of Directors and team. Journey Watch Hedera's journey to build an empowered digital future for all. Transparent Governance Public Policy Hedera's mission is to inform policy and regulation that impact the industry. Meeting Minutes Immutably recorded on Hedera. Roadmap Follow Hedera's roadmap in its journey to build the future. Resources Company What's New Partners Papers Careers Media Blog Technical Press Podcast Community Events Meetups Store Brand Navigation QUICKSTART Coq Proof Completed By Carnegie Mellon Professor Confirms Hashgraph Consensus Algorithm Is Asynchronous Byzantine Fault Tolerant news Oct 17, 2018 by Hedera Team Hedera is the most used, sustainable, enterprise-grade public network for the decentralized economy. Asynchronous Byzantine Fault Tolerance (ABFT) Is the ‘Gold Standard’ for Security in Distributed Systems Dallas TX, Hedera18 Developer Conference – October 17, 2018 – Hedera Hashgraph, a next-generation distributed public ledger with highly diversified governance, today announced that the hashgraph consensus algorithm has been validated as asynchronous Byzantine Fault Tolerant (ABFT) by a math proof checked by computer using the Coq system. This proves the claims stated in the hashgraph tech report that hashgraph is ABFT — mathematically the highest possible level of security for distributed systems. Dr. Leemon Baird will present a session today on formal methods at Hedera18, the inaugural hashgraph developer conference. Interested participants can join the live stream at no charge, at learn.hederahashgraph.com/livestream. Coq is 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. Unlike most math proofs that are merely checked by humans, a Coq proof is actually checked by a computer. This avoids some of the mistakes that humans can make when reading a proof. The verification was conducted through the Coq Proof Assistant, which checks that the proof is correct, and was completed by Karl Crary, Associate Professor of Computer Science at Carnegie Mellon University. The proof can be found at https://www.hedera.com/hashgraph-coq.zip. “This is just the beginning,” said Dr. Leemon Baird, Chief Scientist of Hedera. “Formalized methods like these, where a computer verifies a math proof of correctness, are the future of software, wherever security and trust are critical.” Hedera plans to continue to create additional Coq system proofs, to prove the correctness of additional efficiency improvements, and eventually to ensure that the software implementing the algorithm is also correct. Asynchronous Byzantine Fault Tolerance For over three decades, Byzantine fault tolerance (BFT) has been the standard for security in distributed systems. Byzantine fault tolerance means that honest members of a network can be guaranteed to agree on a common consensus, even if malicious members (Byzantine nodes) are trying to prevent that consensus, or trick them into reaching different conclusions. A system is BFT if it can guarantee that there will come a moment in time when all nodes agree on consensus, and they know they’ve reached consensus, and it is always the same consensus. BFT means achieving this even while allowing for a wide range of faults or attacks. Byzantine faults include behaviors like lying, collusion, and selective non-participation. Clearly it will be harder for a set of nodes to come to consensus under these sorts of errors, compared to simpler scenarios where nodes may just crash. The strongest form of BFT is asynchronous. An ABFT system allows for the possibility of some messages between honest members being delayed arbitrarily long, or not making it to their intended recipients at all. The adversary might even control the network itself, at least partially. This is the gold standard for distributed consensus. A truly secure distributed ledger technology (DLT) must be able to achieve consensus under this assumption. Algorithms may claim to support ‘partially’ asynchronous BFT, where messages are never delayed by more than a certain period of time, and always get through by that deadline. But today’s reality is that many kinds of attackers can prey on exactly this assumption, to either bring a network to its knees, or disrupt the order of transactions. Botnets, Distributed Denial of Service (DDoS) attacks, and malicious firewalls can all interfere with messages. As such, ‘partially’ asynchronous BFT will not provide for reliable, real-world systems in the long run. As Hedera builds an internet-wide trust layer that could eventually process trillions of dollars worth of transactions, we must ensure that we apply the strongest security principles possible to deal with such attacks. With the new Coq proof, Hedera becomes the first public ledger that has a computer-verified mathematical proof that it is truly asynchronous BFT. It guarantees consensus will be achieved, we will know it when it happens, and we will all reach the same consensus, and do so even under realistic assumptions about malicious nodes and network errors. ### About Hedera The Hedera hashgraph platform will offer a distributed public ledger with highly diversified governance that enables anyone to easily develop globally decentralized applications. Developers can build secure, fair, blazing-fast decentralized applications on top of the Hedera hashgraph platform. For more information, visit hedera.com, or follow us on Twitter at @hashgraph, Telegram at t.me/hederahashgraph, or Discord at hedera.com/discord. The Hedera whitepaper can be found at hedera.com/whitepaper. For Media Inquiries Zenobia Godschalk E: [email protected] T: 1.833.794.7537 x 717 Share This Back to blog What is gRPC, gRPC-Web, and Proxies? Ed Marquez Pragmatic Blockchain Design Patterns – Integrating Blockchain into Business Processes Michiel Mulders Zero Cost EthereumTransaction on Success: Hedera's New Fee Model for Relay Operators Oliver Thorn Hedera Adopts Chainlink Standard for Cross-Chain Interoperability To Accelerate Ecosystem Adoption Hedera Team Hedera Developer Highlights March 2025 Michiel Mulders Hedera Release Cycle Overview Ed Marquez View All Posts Sign up for the newsletter CONNECT WITH US Transparency Open Source Audits & Standards Sustainability Commitment Carbon Offsets Governance Hedera Council Public Policy Treasury Management Meeting Minutes LLC Agreement Node Requirements Community Events Meetups HBAR Telegram Developer Discord Twitter Community Support FAQ Network Status Developer Discord StackOverflow Brand Brand Guidelines Built on Hedera Logo Hedera Store About Team Partners Journey Roadmap Careers Contact General Inquiry Public Relations © 2018-2025 Hedera Hashgraph, LLC. All trademarks and company names are the property of their respective owners. All rights in the Deutsche Telekom mark are protected by Deutsche Telekom AG. All rights reserved. Hedera uses the third party marks with permission. Terms of Use  |  Privacy Policy