Sonic Labs Releases Open-Source Library for DAG Protocol Verification

Sonic Labs, the platform behind the layer-1 (L1) Sonic blockchain, has released an open-source formal verification library specifically designed for Directed Acyclic Graph (DAG) consensus protocols. This library, announced on Wednesday, June 25, aims to enhance the security and efficiency of blockchain development by providing developers with the tools to model and verify the correctness of complex DAG protocols through mathematical proof.

The library features modular, reusable components, which streamline the process of ensuring the integrity and reliability of blockchain systems. Developed in collaboration with logic experts from the University of Sydney and INRIA using TLA+, a formal specification language, the library helps developers leverage mathematical proof to verify the correctness of DAG protocols, even those running on Sonic’s own Ethereum (ETH) Virtual Machine (EVM) blockchain.

Dr. Bernhard Scholz, Chief Research Officer at Sonic Labs, highlighted the importance of this development in addressing security failures in blockchain technology. He noted that blockchain security failures often stem from undiagnosed problems that are only detected once it’s too late. With this library, Sonic Labs aims to shift from relying on hope to providing mathematical proof, offering the tools to verify, with certainty, that a protocol will behave safely under all conditions. The goal is to make formal verification accessible to every protocol developer, thereby enhancing the overall security of blockchain networks.

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 this issue by giving developers the tools needed to verify the protocol is safe with mathematical certainty. By using formal verification, a method long used in industries such as aerospace and finance, Sonic Labs aims to eliminate entire classes of errors 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 enhancing security, 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 is aimed at strengthening the broader Web3 ecosystem by giving all projects of all sizes access to industrial-grade verification tools. By providing developers with powerful tools to verify the correctness of their protocols, Sonic Labs is helping to build a more secure and reliable blockchain ecosystem. This development is expected to have a positive impact on the broader blockchain community, as it enables developers to create more robust and trustworthy systems.