Sonic Labs Releases Formal Verification Library: What to Know

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. Now available as an open source project, the development is helmed by Chief Research Officer Dr. Bernhard Scholz.

Sonic Labs unveils verification library for DAG-based networks

According to the official statement by Sonic Labs, its team released and fully open-sourced a formal verification library for DAG-based consensus protocols. The new instrument leverages 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.

Dr. Bernhard Scholz, Chief Research Officer of Sonic Labs, outlines that accessibility for new cohorts of blockchain developers is the primary focus for the new release:

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.

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.

Making protocol verification more inclusive and cost-effective than ever before

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 in all possible scenarios, leaving no room for error.

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 in proving the integrity of DAG-based consensus.