Certora has taken a significant step towards improving smart contract security by open-sourcing its advanced formal verification tool, the Certora Prover. This technology, designed for Ethereum’s EVM, Solana’s sBPF, and Stellar’s WASM, is now freely available to developers. By leveraging this tool, projects can enhance the security, transparency, and community-driven nature of their smart contracts without incurring additional costs.
The Certora Prover has been in continuous development for over seven years and has contributed to securing assets worth more than $100 billion in total value locked (TVL) across multiple projects. Some of the notable names benefiting from this technology include Aave, MakerDAO, Uniswap, Lido, EigenLayer, Solana Foundation, Ether.fi, Silo, Safe, Kamino, Squads, Jito, Manifest, Morpho, and Balancer. Over the years, developers have defined more than 70,000 verification rules to improve smart contract security. Unlike traditional security audits and testing, formal verification provides mathematical proof of security by detecting all possible vulnerabilities and confirming their absence.
Addressing the Cost and Accessibility Challenges of Web3 Security
Certora’s leadership has emphasized the importance of making security accessible to a broader range of developers. The company aims to eliminate the financial and educational barriers that have traditionally restricted robust security measures to well-funded teams. The decision to open-source the Certora Prover aligns with the goal of making secure smart contracts the industry standard rather than an exclusive advantage.
Despite significant expenditures on security audits, Web3 projects continue to face challenges in preventing vulnerabilities. Many decentralized finance (DeFi) projects invest millions in security assessments and take extensive time before launching, yet financial risks persist. Although the frequency of major exploits has declined, securing smart contracts remains costly and unattainable for many developers. By releasing the Certora Prover as an open-source tool, the company aims to democratize access to advanced verification methods and significantly reduce security-related expenses.
How the Certora Prover Strengthens Smart Contract Security
Certora has positioned formal verification as an essential component of the smart contract development process. Unlike conventional auditing techniques, which rely on predefined test cases, formal verification mathematically guarantees security by systematically identifying and eliminating vulnerabilities. The Certora Prover acts as an automated security analyst, reviewing smart contract code based on developer-defined rules. It can, for instance, validate that no user—including malicious actors—can withdraw more assets than they have deposited. Unlike traditional testing that examines only selected scenarios, the Prover evaluates all potential outcomes, ensuring no undetected exploits remain.
This technology has already demonstrated its effectiveness by uncovering critical security flaws before deployment. The Certora Prover identified a long-standing issue in MakerDAO’s DAI equation that had gone unnoticed since 2018. Additionally, it detected a vulnerability in SushiSwap’s Trident pools that could have led to liquidity loss and a flaw in PRBMath’s rounding logic that posed risks to liquidity providers. These findings highlight that even widely used protocols subjected to multiple audits can still contain hidden vulnerabilities that only formal verification can expose.
A New Era of Open-Source Security for Web3
By making the Prover openly available, Certora is fostering an environment where security becomes a fundamental aspect of smart contract development rather than an afterthought. Integrating formal verification at the early stages of development can help projects reduce security expenses and mitigate risks before deployment. With support for Ethereum, Solana, and Stellar, the Prover provides a robust security solution across multiple blockchain ecosystems.
Certora is encouraging developers, security researchers, and the wider Web3 community to engage with this initiative. Developers can immediately start using the Prover to verify their smart contracts, while security professionals have the opportunity to participate in Certora’s security competitions. These initiatives aim to strengthen the security of major DeFi projects while offering rewards for valuable contributions.
Through this open-source initiative, Certora aims to set a new industry standard for smart contract security, making robust protection measures accessible to all blockchain developers.
