Sonic Labs Unveils Formal Verification Library For DAG Consensus Protocols
In Brief
Sonic Labs has launched an open-source formal verification library to mathematically ensure the security and reliability of DAG-based blockchain consensus protocols as blockchain ecosystems continue to grow in value.
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.
Disclaimer
In line with the Trust Project guidelines, please note that the information provided on this page is not intended to be and should not be interpreted as legal, tax, investment, financial, or any other form of advice. It is important to only invest what you can afford to lose and to seek independent financial advice if you have any doubts. For further information, we suggest referring to the terms and conditions as well as the help and support pages provided by the issuer or advertiser. MetaversePost is committed to accurate, unbiased reporting, but market conditions are subject to change without notice.
About The Author
Alisa, a dedicated journalist at the MPost, specializes in crypto, AI, investments, and the expansive realm of Web3. With a keen eye for emerging trends and technologies, she delivers comprehensive coverage to inform and engage readers in the ever-evolving landscape of digital finance.
More articles
Alisa, a dedicated journalist at the MPost, specializes in crypto, AI, investments, and the expansive realm of Web3. With a keen eye for emerging trends and technologies, she delivers comprehensive coverage to inform and engage readers in the ever-evolving landscape of digital finance.
