Sonic Labs, the team behind EVM L1 Sonic, has announced a major breakthrough in blockchain security with the release of a formal verification library for DAG-based consensus protocols. The development, now available as an open source project, is directed by Chief Research Officer Dr. Bernhard Scholz.
Sonic Labs announces a DAG-based network verification library
According to an official statement from Sonic Labs, the team has released a formal verification library for DAG-based consensus protocols and is now fully open. The new device leverages formal verification to mathematically prove the safety of the directed acyclic graph blockchain, including Sonic’s proprietary EVM blockchain.
It flows through the blockchain, what happens if the code doesn’t work?
Sonic uses formal verification to mathematically prove that the DAG consensus protocol is not broken.
https://t.co/jxfv1vuo44 pic.twitter.com/xpqd9hbrbo
– Sonic Labs (@soniclabs) June 25, 2025
The Sonic Labs validation library was built using the Sonic Labs validation library using the TLA+ Proof Assistant. By providing reusable modular components, it simplifies the process of verifying DAG-based consensus protocols. These allow developers to model and validate protocols with minimal effort.
Dr. Bernhard Scholz, Chief Research Officer at Sonic Labs, outlines accessibility to a new cohort of blockchain developers is the main focus of new releases.
In blockchain, security failures are often attributed to assumptions that have not been tested until it is too late. This library provides tools to move from hope to proof and verify that protocols operate safely under all conditions with mathematical certainty. Our goal is to ensure that all protocol developers have access to formal verification.
The library contains evidence for prominent DAG-based protocols such as DAG-Rider, Cordial Miner, Bullshark, Hashgraph, and Aleph, and has Sonic’s own consensus protocol validated as derivatives. The work, first announced at NASA Formal Method 2025 (NFM 2025) in Williamsburg, Virginia on June 11-13, sets a new benchmark for blockchain security.
Make protocol verification more comprehensive and cost-effective than ever
With trillions of dollars trapped in the blockchain, the vulnerability of the consensus protocol could lead to catastrophic exploits such as double spending and ledger inconsistencies. Traditional testing and auditing are often lacking because it cannot guarantee that it is bug free. Sonic Labs addressed this challenge by adopting formal verification, a rigorous mathematical approach that proves that the protocol is safe in all possible scenarios. There is no room for error.
In addition to supporting validation of existing protocols, Sonic Labs’ solutions help designers attempt to create new DAG-based protocols or modify existing models. To demonstrate the effectiveness of its library, Sonic Lab has begun to deploy formal verification, proving that unsafe behavior is mathematically impossible on the Sonic blockchain.
Sonic Labs aims to empower blockchain developers to build validated, secure protocols by open-sourcing libraries. This will strengthen the entire Web3 ecosystem and dramatically reduce the time and cost involved in proving the integrity of a DAG-based consensus.
