Trusted Editorial content, reviewed by leading industry experts and seasoned editors. Ad Disclosure
Sonic Labs has been living up to its name and toiling away in the lab on a new research paper. It ain’t merely no theoretical document either: it’s yielded a tangible application within the field of blockchain consensus, and the formal verification library Sonic Labs has developed is now open-sourced and available on Github.
The Sonic Labs team is of course best known for architecting the Sonic Layer-1 chain that rose from the ashes of Fantom. Sonic uses a DAG (Directed Acyclic Graph) for its consensus, and it was this area where the Labs team understandably chose to focus their efforts. While the subsequent verification library they’ve developed has implications for Sonic’s EVM network, it’s equally applicable on all existing and future DAG-based chains, where it has the potential to significantly enhance security by preventing bugs from creeping in.
Blockchain consensus design is big brain stuff that calls for the expertise of researchers spanning mathematics, cryptography, and game theory. While the Sonic Labs team is well schooled in these areas, it called in a few experts to help with its deep dive into DAGs with the goal of making them verifiably secure.
Developed in partnership with top logicians from the University of Sydney and INRIA, the library leverages the TLA+ proof assistant to provide modular, reusable components. These simplify the verification process for developers, enabling them to model and confirm the safety of DAG-based protocols with ease. The library includes verified proofs for major protocols such as DAG-Rider, Cordial Miner, Bullshark, Hashgraph, and Aleph, with Sonic’s own consensus protocol validated as a derivative.
Given the value that now courses through blockchain ecosystems, it’s in everyone’s interests to make them safer. This is easier said than done, however, since standard auditing procedures are by no means fool-proof and it’s not unheard of for vulnerabilities to creep in that are later exploited with devastating consequences.
Sonic Labs’ formal verification approach uses rigorous mathematical proofs to eliminate errors, ensuring that protocols perform reliably in every conceivable scenario. The library not only verifies existing protocols but also empowers developers to design new DAG-based systems or refine current ones. Sonic Labs has already applied its proprietary tool to prove that unsafe behavior is mathematically impossible on the Sonic blockchain.
First showcased at NASA Formal Methods 2025 in Williamsburg, Virginia in mid-June, the library adds a valuable defensive tool to the arsenal of blockchain developers. As modular design becomes the default way of building blockchains, the risk of security risks creeping in rises. For example, many Blockchain-as-a-Service providers allow teams to create and deploy a custom network in just a few clicks. But should they elect to alter the parameters of the consensus mechanism in the process, there’s a possibility of unwittingly introducing a security hole.
This is just one area in which Sonic Labs’ formal verification library has clear application. But it’s also got value to add in appraising existing DAG-based chains. Vulnerabilities can often lie undiscovered for years in the wild before, in a best-case scenario, a whitehat spots it and it’s patched. In the worst case, it falls into the hands of a blackhat who’s able to exploit it.
As Sonic Labs’ Chief Research Officer Dr. Bernhard Scholz summarizes, “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.” With the open-source library now available to web3 developers, the onus is on them to take this tool and make the most of it.
