Sonic Labs has introduced a groundbreaking open-source library aimed at elevating the security of decentralized networks through formal verification of Directed Acyclic Graph (DAG)-based blockchain consensus protocols. Developed in collaboration with academic researchers from the University of Sydney and the French research institute INRIA, the initiative is designed to reduce the risk of flaws in blockchain infrastructure by offering mathematical assurance of protocol correctness.
The formal verification library was unveiled earlier this month at NASA Formal Methods 2025 (NFM 2025), held in Williamsburg, Virginia. The tool is built using TLA+, a formal specification language created by Microsoft Research, which allows developers to construct mathematical models to verify whether a protocol functions reliably under every possible scenario.
Sonic Labs stated that the library aims to streamline the process of modeling complex distributed systems. It does this by offering modular, reusable components that can be adapted across various blockchain consensus designs. This flexibility is expected to support a wide range of developers in both validating existing systems and building secure protocols from the ground up.
A number of well-known DAG-based consensus protocols have already been verified using the tool, including DAG-Rider, Cordial Miner, Bullshark, Hashgraph, and Aleph. Sonic Labs has also confirmed that its own EVM-compatible consensus mechanism has been formally validated as a derivative model using the same framework.
Dr. Bernhard Scholz, Chief Research Officer at Sonic Labs, emphasized that the tool enables a shift from assumptions to certainties. He conveyed that the library provides developers with the means to mathematically ensure the safe behavior of protocols under all operational conditions. This advancement is particularly significant given that blockchains today secure assets worth trillions of dollars, creating enormous pressure on underlying infrastructure to perform flawlessly.
Trillions flow through blockchains, but what if the code goes wrong?
At Sonic, we use formal verification to mathematically prove that our DAG consensus protocol can’t break.
🔗 https://t.co/JxFv1VUo44 pic.twitter.com/XpQD9hBRBO
— Sonic Labs (@SonicLabs) June 25, 2025
Despite the widespread use of audits and penetration tests across the blockchain industry, experts agree that such methods cannot guarantee the complete elimination of critical bugs—especially in asynchronous and highly complex systems. Sonic Labs asserted that formal verification presents a robust alternative by delivering mathematical proof of safety, thereby addressing gaps that conventional testing cannot cover.
Internally, Sonic Labs has already begun utilizing the library to verify its own blockchain network. The company indicated that the tool can confirm the impossibility of unsafe behavior within the bounds of clearly defined conditions. By releasing it as open-source, the firm aims to lower barriers to entry for secure system design and encourage widespread use of formal verification in the Web3 space.
Sonic operates as an EVM-compatible blockchain optimized for high throughput. The network boasts sub-second transaction finality and the capacity to handle up to 400,000 transactions per second. It also features a Fee Monetization model that allows decentralized application (dApp) developers to earn up to 90% of the transaction fees generated by their apps.
As the financial value and complexity within blockchain networks continue to grow, even minor flaws in consensus mechanisms can trigger massive losses and erode user confidence. With the introduction of this new verification tool, Sonic Labs aims to fill a critical gap by introducing mathematically grounded assurance into blockchain development—ultimately setting a new standard for security in decentralized ecosystems.
