Sonic Labs, the platform behind the layer-1 (L1) Sonic blockchain, has released an open-source formal verification library designed specifically for Directed Acyclic Graph (DAG) consensus protocols, as per the reports shared with Finbold on Wednesday, June 25.
With modular, reusable components, the library helps developers leverage mathematical proof to model and verify the correctness of complex DAG protocols, even those running on Sonic’s own Ethereum (ETH) Virtual Machine (EVM) blockchain.
The project was developed in collaboration with logic experts from the University of Sydney and INRIA using TLA+, a formal specification language developed.
Dr. Bernhard Scholz, Chief Research Officer at Sonic Labs, noted that blockchain security failures are often the result of undiagnosed problems that are only detected once it’s too late:
“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
With billions in value locked on-chain, the need to prevent exploits like double spends or ledger divergence has never been greater.
The new Sonic Labs library addresses the issue by giving developers the tools needed to verify the protocol is safe with mathematical certainty.
Namely, by using formal verification, a method long used in industries such as aerospace and finance, Sonic Labs aims to eliminate entire classes in preparation for protocol deployment.
The library already includes verified proofs for a wide range of DAG protocols, including DAG-Rider, Cordial Miner, and Bullshark, with Sonic’s own protocol verified as a derivative.
In addition to security buffs, the library also features tools for developers of all levels to prototype new DAG-based systems more efficiently.
To drive the point home, Sonic Labs is open-sourcing the entire library, making it available on GitHub.
This move, the company says, will help strengthen the broader Web3 ecosystem by giving all projects of all sizes access to industrial-grade verification tools.
