Certora Open-Sources the Certora Prover, Bringing Industrial-Grade Formal Verification to the Web3 Community
Tel Aviv, Israel, February 24th, 2025, Chainwire
Certora is making smart contract security more accessible by open-sourcing the Certora Prover, the most advanced formal verification engine for Ethereum (EVM), Solana (sBPF) and Stellar (WASM). Developers can now leverage this powerful tool for free, ensuring their smart contracts are secure, transparent, and community-driven.
What is Certora Prover?
The Certora Prover has been in development for over seven years and has secured more than $100 billion in total value locked (TVL) across projects including Aave, MakerDAO, Uniswap, Lido, EigenLayer, Solana Foundation, Ether.fi, Silo, Safe, Kamino, Squads, Jito, Manifest, Morpho, and Balancer. Developers have already written over 70,000 verification rules. Unlike auditing and testing, formal verification is the only method that guarantees security by identifying all possible bugs and ultimately 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 Certora CEO Mooly Sagiv.
“Security remains one of the biggest challenges in Web3. DeFi projects spend millions on audits and often take over a year to launch, yet vulnerabilities continue to put billions of dollars at risk,” said Certora CTO Shelly Grossman. “While high-profile exploits have become less frequent, securing smart contracts remains expensive and out of reach for many developers. That changes today.”
Proven Prover performance
Certora makes formal verification a standard part of the development process. Unlike traditional audits and testing, formal verification mathematically guarantees security by detecting all possible bugs and proving their absence. The Certora Prover acts as an automated mathematical auditor, analyzing a smart contract code and developer-defined rules to provide proof of correctness or counterexamples that reveal vulnerabilities. A developer can define a rule ensuring that no user, even a malicious one, can withdraw more assets than they have deposited. Instead of testing limited scenarios, the Prover evaluates every possible case, ensuring that no hidden exploits exist.
Certora’s formal verification technology has already caught critical vulnerabilities before deployment. The Prover identified a fundamental flaw in MakerDAO’s DAI equation that had gone undetected since 2018, a bug in SushiSwap’s Trident pools that could have led to liquidity drains, and an issue in PRBMath’s rounding logic that posed risks to liquidity providers. These findings demonstrate that even widely used protocols with multiple audits can contain vulnerabilities that only formal verification can uncover.
“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.”
By open-sourcing the Prover, Certora is making advanced security accessible to all developers. Formal verification can now be integrated early in the development process, reducing audit costs and preventing exploits before they happen. The Prover supports Ethereum, Solana and Stellar, allowing projects across multiple chains to benefit from automated, mathematically sound security.
Available now
Certora is inviting developers, security researchers, and the broader Web3 community to join this effort. Developers can start using Prover today to verify their smart contracts, while security researchers can participate in Certora’s competitions to help secure major DeFi projects and earn rewards.
About Certora
Certora is a blockchain security company that provides industry-leading formal verification tools and smart contract audits. Certora’s flagship security product, Prover, is helping protocols like Aave, Lido, and Maker integrate the power of formal verification into their development pipeline to catch even the rare & hard-to-find bugs.
