- The open-source library mathematically demonstrates the security of Directed Acyclic Graph blockchains, such as Sonic’s own EVM blockchain, via formal verification.
- Sonic, has announced a significant advancement in blockchain security with the introduction of a formal verification library.
Under the direction of Chief Research Officer Dr. Bernhard Scholz, Sonic Labs, the team behind the high-performance layer-1 blockchain Sonic, has announced a significant advancement in blockchain security with the introduction of a formal verification library for DAG-based consensus protocols. The open-source library mathematically demonstrates the security of Directed Acyclic Graph blockchains, such as Sonic’s own EVM blockchain, via formal verification.
Sonic Labs’ verification library was built using the TLA+ proof assistant in partnership with top logicians from INRIA and the University of Sydney. It provides modular, reusable components that make the process of verfiying DAG-based consensus protocols easier. These make it easy for developers to model and verify protocols.
Sonic’s own consensus protocol has been verified as a variant of the library, which also contains proofs for well-known DAG-based protocols including DAG-Rider, Cordial Miner, Bullshark, Hashgraph, and Aleph. The work establishes a new standard for blockchain security and was first presented at NASA Formal Methods 2025 (NFM 2025) in Williamsburg, Virginia, on June 11–13.
Dr. Bernhard Scholz, Chief Research Officer, Sonic Labs stated:
“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.”
With trillions of dollars locked in blockchains, flaws in consensus protocols might result in disastrous exploits like ledger discrepancies or double spending. Conventional audits and testing often fail because they are unable to ensure that there are no problems. In order to overcome this difficulty, Sonic Labs has used formal verification, a rigorous mathematical technique that establishes a protocol’s security in any case and eliminates every possibility of mistake.
Sonic Labs’ solution helps designers who want to develop new DAG-based protocols or alter pre-existing models, in addition to facilitating the verification of current protocols. Sonic Labs has started using formal verification to show that dangerous activity is mathematically impossible on the Sonic blockchain, proving the effectiveness of its library.
Sonic Labs hopes to enable blockchain developers to create verifiably safe protocols by making the library open-source. In addition to significantly cutting down on the time and expense required to demonstrate the integrity of DAG-based consensus, this will fortify the whole Web3 ecosystem.
The next generation of DeFi apps is powered by Sonic, the best-performing EVM blockchain, which combines speed, incentives, and top-notch infrastructure. The network can process up to 400,000 transactions per second and reach sub-second finality.
Fee Monetization, a technique that enables developers to get 90% of the network fees earned by their applications, is the foundation of Sonic’s incentive strategy. FeeM, which was inspired by Web2 ad-revenue sharing models, pays developers for increasing growth, consumption, and real activity.
