Certora has announced the open-sourcing of its Certora Prover, a formal verification engine designed to enhance smart contract security on Ethereum (EVM), Solana (sBPF), and Stellar (WASM).
By making this tool freely available, Certora aims to improve security accessibility across the Web3 ecosystem.
The Certora Prover has been developed over seven years and has played a key role in securing more than $100 billion in total value locked (TVL) across projects such as Aave, MakerDAO, Uniswap, and Lido.
Formal verification, unlike traditional audits and testing, mathematically guarantees security by detecting all possible bugs and proving their absence.
“Smart contract security should not be a privilege reserved for well-funded teams or highly educated people. Open-sourcing the Certora Prover is a step toward making bulletproof smart contracts the norm,” said Mooly Sagiv, CEO of Certora.
The Certora Prover: Enhancing Web3 Security with Formal Verification
Smart contract vulnerabilities continue to pose a major risk in the DeFi space, with exploits leading to billions in losses despite extensive audits. Notably, Certora’s technology provides an automated mathematical auditing system that evaluates smart contract code against predefined security rules.
“The Prover is a powerful tool to ensure that funds stay where they’re supposed to stay,” said Certora CTO Shelly Grossman. “We’ve been building this for a long time and we’re excited to release it to the community.”
Unlike conventional testing, which evaluates limited scenarios, the Certora Prover assesses every possible execution path within a smart contract. This process has identified critical vulnerabilities in widely used protocols, including:
A flaw in MakerDAO’s DAI equation undetected since 2018.A bug in SushiSwap’s Trident pools that could have led to liquidity drains.An issue in PRBMath’s rounding logic that posed risks to liquidity providers.
Making Security More Accessible
By open-sourcing the Certora Prover, the company is enabling developers to integrate formal verification early in the development cycle, reducing audit costs and mitigating security risks before deployment.
In addition, the tool supports multiple blockchain networks, allowing developers from various ecosystems to adopt a proactive approach to security.
Certora is also engaging security researchers through competitions that incentivize vulnerability detection in major DeFi projects. Developers can start using the Prover immediately to verify their smart contracts and improve protocol security.
