Formal Methods: The Importance of Being ABFT in a World with… | 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 Formal Methods: The Importance of Being ABFT in a World with Bad Actors technical Oct 29, 2018 by Hedera Team Hedera is the most used, sustainable, enterprise-grade public network for the decentralized economy. In the past year, over $1 billion in cryptocurrency has been stolen by hackers. There have also been denial of service attacks that have shut down other types of servers for hours. For example, a 2016 DDoS attack (executed via a botnet consisting of a large number of  compromised internet connected devices) against DNS (Domain Name System) provider Dyn caused major internet services to be unavailable for many users across North America and Europe for a number of hours. If public distributed ledgers continue to grow, these networks could eventually have trillions of dollars of value flowing through them — and similar disruptive cyberattacks are bound to follow. That’s why, before using distributed ledgers, enterprises and careful consumers will demand that the platforms demonstrate the highest possible levels of network security. The highest security standard for consensus algorithms is known as Asynchronous Byzantine Fault Tolerance (ABFT). The hashgraph algorithm, as used in the Hedera public ledger, achieves this gold standard, with a mathematical proof that it is ABFT. This proof-of-stake consensus system was first proved to be ABFT in a rigorous math proof published in 2016. That proof has now been verified by computer in a formal verification completed by a Carnegie Mellon University professor — and we think it is important to explain what that means. If you’re reading the Hedera blog, you’re probably familiar with the Byzantine Generals Problem (if not, here’s a short explainer). The problem is for a distributed group to achieve consensus on a set of transactions when you can’t trust all the members of the group, nor the network over which they communicate. In a public ledger where anyone can run a node, you can’t trust all of the nodes to be honest, as a bad actor could stand up a node, or create a firewall, or launch a set of attacking computers. They could seek to disrupt consensus by delaying transactions or otherwise corrupting things. Byzantine fault tolerance means that the honest members of a network can be guaranteed to agree on the timing and order of a set of transactions, even if almost ⅓ of the influence of the nodes is maliciously trying to prevent that consensus. Or to trick the honest nodes into reaching different conclusions, or even if to attack the internet itself. But more than that, a Byzantine Fault Tolerant (BFT) system must deliver finality of consensus. This means there will come a moment in time when a node knows it has achieved consensus, and that all participating nodes will reach the same consensus, and that there is zero chance that the consensus will change. However, there is another aspect to consider — whether this can still be achieved when there are attacks on the internet itself. Intuitively, if an honest node does not receive a message it expects, it cannot easily distinguish between that message being sent by an another honest node but subsequently being lost by the network, or a dishonest node not sending the message in the first place. The more unreliable the network is with respect to delivery of messages, the more challenging is consensus — and so accordingly the more challenging to achieve BFT. Some consensus algorithms have proofs that they are BFT, but the proofs rely on simplifying assumptions about the network’s reliability with respect to message delivery — assumptions that do not reflect the reality of today’s internet — a reality that includes firewalls, botnets, DDoS attacks, worms, and viruses that can impact message delivery. For example, so called partially synchronous BFT or partially asynchronous BFT systems make the assumption that messages are never lost and will always arrive within some known bound. With such an assumption, nodes can reliably deduce whether another node is faulty. But this assumption doesn’t match reality. A much stronger version of BFT, one that better acknowledges today’s network reliability, is asynchronous BFT (ABFT). Rather than assuming 100% reliability, and assuming some maximum message latency, ABFT systems allow for messages to be lost or indefinitely delayed  — assuming only that an honest node’s messages will eventually get through. It is much more challenging for an honest node to assess whether another node is not following the rules, if that node’s messages can be indeterminately delayed. It is challenging to make consensus asynchronous BFT. But it better reflects the reality of networks than pretending we can assume synchronous or partially synchronous. The importance of ABFT has been widely recognized among computer scientists, but for decades it could not be achieved at scale. This changed with Dr. Leemon Baird’s invention of the proof-of-stake hashgraph consensus algorithm used by Hedera, which he proved mathematically to be ABFT in his 2016 tech report, and published again in the Hedera whitepaper. While other mathematicians have verified the proof of hashgraph being ABFT, additional confidence in its correctness is possible. Formal methods is the process of having a computer check whether a system (such as an algorithm or piece of software) satisfies some set of requirements or properties (such as ABFT). This starts with writing a math proof in the traditional form, and then working to put it in a form that a computer can check. This verifies an algorithm's properties in a more thorough fashion than just having humans read it. Coq is a formal proof assistant system that provides a formal language to write mathematical definitions and axioms and theorems, together with an environment for interactive development of machine-checked proofs. We are now pleased to announce additional validation of hashgraph’s ABFT status. A Carnegie Mellon professor has completed a computer-checked math proof using Coq, that verifies that the hashgraph algorithm used by Hedera is ABFT. With this new proof, the Hedera platform becomes the first public, proof-of-stake, distributed ledger that has a computer-verified mathematical proof that it is ABFT. Our announcement on the Coq proof can be found at https://hedera.com/blog/coq-proof-completed-by-carnegie-mellon-professor-confirms-hashgraph-consensus-algorithm-is-asynchronous-byzantine-fault-tolerant. The ultimate vision, as part of our ongoing commitment to the long-term security of the Hedera platform, is for every layer of the stack to be verified with the same rigor — from algorithms to software to even hardware. The Coq proof validates the original proof that Hedera’s foundational algorithm is ABFT. The next step is to verify efficiency tweaks to the algorithm, and then to verify that the consensus software correctly implements it. So stay tuned! To download and run the Coq scripts, visit https://hedera.com/platform#security. 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