Sonic Labs, the team behind high-performance layer-1 blockchain Sonic, has announced a major breakthrough in blockchain security with the release of a formal verification library for DAG-based consensus protocols, led by Chief Research Officer Dr. Bernhard Scholz. The open-source library uses formal verification to mathematically prove the safety of Directed Acyclic Graph blockchains, including Sonic’s own EVM blockchain.
Developed in collaboration with leading logicians from the University of Sydney and INRIA, Sonic Labs’ verification library has been built using the TLA+ proof assistant. It simplifies the process of verifying DAG-based consensus protocols by offering reusable, modular components. These allow developers to model and verify protocols with minimal effort.
The library includes proofs for prominent DAG-based protocols like DAG-Rider, Cordial Miner, Bullshark, Hashgraph, and Aleph, with Sonic’s own consensus protocol verified as a derivative. First presented at NASA Formal Methods 2025 (NFM 2025) in Williamsburg, Virginia, on June 11-13, the work sets a new benchmark for blockchain security.
“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.”
— Dr. Bernhard Scholz, Chief Research Officer, Sonic Labs
With trillions of dollars locked in blockchains, vulnerabilities in consensus protocols can lead to catastrophic exploits such as double spending or ledger inconsistencies. Traditional testing and audits often fall short as they cannot guarantee the absence of bugs. Sonic Labs has addressed this challenge by employing formal verification, a rigorous mathematical approach that proves a protocol is secure under all possible scenarios, leaving no room for errors.
In addition to supporting the verification of existing protocols, Sonic Labs’ solution assists designers seeking to create new DAG-based protocols or modify existing models. To demonstrate the efficacy of its library, Sonic Labs has begun deploying formal verification to prove that unsafe behavior is a mathematical impossibility on the Sonic blockchain.
By open-sourcing the library, Sonic Labs aims to empower blockchain developers in the construction of verifiably secure protocols. This will strengthen the entire Web3 ecosystem while dramatically reducing the time and cost involved with proving the integrity of DAG-based consensus.