Team behind the high-performance Layer 1 blockchain Sonic, Sonic Labs introduced a formal verification library designed to enhance security in DAG-based consensus protocols. Led by Chief Research Officer Dr. Bernhard Scholz, the library aims to provide mathematical proof of safety for Directed Acyclic Graph (DAG) blockchains, including Sonic’s own EVM-compatible network.
Developed in partnership with researchers from the University of Sydney and INRIA, the open-source library is built using the TLA+ proof assistant. It offers a modular and reusable framework that streamlines the process of modeling and verifying consensus mechanisms based on DAG architecture.
The verification library features formal proofs for several existing DAG-based protocols, such as DAG-Rider, Cordial Miner, Bullshark, Hashgraph, and Aleph. Sonic’s proprietary protocol has also been verified as a derivative within this framework. The research was first presented at the NASA Formal Methods 2025 conference, held in Williamsburg, Virginia, from June 11 to 13, and represents a notable advancement in blockchain verification standards.
“In blockchain, security failures often stem from assumptions that go untested until it’s too late,” said Dr. Bernhard Scholz, Chief Research Officer at Sonic Labs, in a written statement. “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,” he added.
As Blockchain Value Surges, Sonic Labs Launches Formal Verification Framework To Ensure Protocol Security And Reliability
As the value secured by blockchain networks continues to grow, the potential impact of vulnerabilities in consensus protocols becomes increasingly significant, with risks including double spending and inconsistent ledger states. Conventional testing and code audits are limited in their ability to guarantee bug-free systems. In response, a formal verification method has been applied by Sonic Labs, utilizing mathematical proofs to confirm protocol security across all possible conditions.
This approach not only validates existing consensus protocols but also aids developers who are designing new Directed Acyclic Graph-based models or adapting current ones. The method is currently being implemented to formally verify that the Sonic blockchain cannot exhibit unsafe behavior, establishing the protocol’s reliability through mathematical validation.
By making the verification library openly available, the initiative provides blockchain developers with resources to build provably secure systems. This is expected to improve the overall resilience of decentralized ecosystems and reduce the resource demands typically associated with consensus protocol verification.
The post Sonic Labs Unveils Formal Verification Library For DAG Consensus Protocols appeared first on Metaverse Post.
