Sonic Labs, the research arm behind the high-performance layer-1 blockchain Sonic, today unveiled an open-source formal verification library designed specifically for Directed Acyclic Graph (DAG) consensus protocols. Led by Chief Research Officer Dr. Bernhard Scholz, the new toolkit has been years in the making and promises to bring mathematical certainty to a class of blockchain designs long prized for their throughput but often criticized for unverified safety guarantees.
First presented this week at NASA Formal Methods 2025 in Williamsburg, Virginia, the library leverages the TLA+ proof assistant—the same rigorous framework used to validate critical aerospace and distributed-system algorithms—to give protocol designers reusable, modular components for building and checking DAG-based consensus under all possible network conditions.
Scholz said, “In blockchain, security failures often stem from assumptions that go untested until it’s too late. With this library, we’re shifting from hope to proof, offering the tools to verify, with mathematical certainty, that a protocol will behave safely under all conditions. Our goal is to make formal verification accessible to every protocol developer.”
Collaboration with Leading Logicians
Sonic Labs developed the library in close partnership with logicians at the University of Sydney and France’s INRIA research institute. Over the past two years, the joint team encoded the core safety properties of five prominent DAG protocols—DAG-Rider, Cordial Miner, Bullshark, Hashgraph and Aleph—then demonstrated how Sonic’s own consensus rules fit naturally as a derivative model.
Building on these foundations, developers can now mix and match verified modules—say, a leader-election component or finality gadget—rather than crafting each proof from scratch. The result: what once took months of painstaking theorem-proving can now be assembled in days, dramatically lowering the barrier to formally verified blockchain research.
Why Formal Verification Matters
Blockchains today secure trillions of dollars in digital assets, yet the traditional defense of audits and testnets cannot guarantee the absence of subtle consensus bugs that might let an attacker double-spend funds or fork the ledger. Formal verification treats the protocol’s specification as a mathematical theorem: if the proof holds, so does the guarantee of safety.
Imagine sending a rocket to space without verifying its guidance system. Blockchains are no less critical. Sonic Labs is giving developers the compass to chart a flight path free of hidden crashes. Sonic Labs has already applied its library to Sonic’s own EVM-compatible network, proving that dangerous scenarios—such as two conflicting blocks reaching finality—cannot occur. The team plans to continue rolling out formal checks across upcoming protocol upgrades and third-party extensions.
Empowering the Web3 Ecosystem
By open-sourcing the library on GitHub, Sonic Labs hopes to spark a wave of collaboration among blockchain teams worldwide. Developers experimenting with novel DAG designs—or tweaking existing protocols—can now lean on battle-tested verification modules, reducing both time and cost for academic research and production deployments.
This announcement arrives amid rapid growth for the Sonic network itself. Boasting sub-second finality and throughput of up to 400,000 transactions per second, Sonic has staked its claim as the fastest EVM blockchain on the market. A novel “Fee Monetization” model pays developers 90% of network fees generated by their decentralized applications—an incentive structure borrowed from Web 2 ad-revenue sharing that has already attracted several DeFi projects seeking predictable, high-performance infrastructure.
With formal verification now part of its toolkit, Sonic Labs aims to further cement Sonic’s reputation as both a bleeding-edge research platform and a rock-solid production chain. For protocol designers and blockchain architects alike, the new library may well set the benchmark for how safety is built into tomorrow’s decentralized systems.
