"Certora Revolutionizes Web3: Open-Sources Advanced Smart Contract Security Tool"

Coin WorldMonday, Feb 24, 2025 10:12 am ET
1min read

Certora, a leading blockchain security company, has made a significant contribution to the Web3 community by open-sourcing the Certora Prover, an advanced formal verification engine for Ethereum (EVM), Solana (sBPF), and Stellar (WASM). This move aims to enhance smart contract security, making it more accessible and affordable for developers.

The Certora Prover, developed over seven years, has already secured over $100 billion in total value locked (TVL) across various projects, including Aave, MakerDAO, Uniswap, and Lido. With over 70,000 verification rules written by developers, the Prover ensures the security of smart contracts by identifying and proving the absence of all possible bugs.

Certora CEO Mooly Sagiv emphasized the importance of making smart contract security accessible to all, stating, "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."

Certora CTO Shelly Grossman highlighted the ongoing challenge of securing smart contracts, noting that while high-profile exploits have become less frequent, securing smart contracts remains expensive and out of reach for many developers. The open-sourcing of the Certora Prover aims to address this issue by making advanced security accessible to all developers.

The Certora Prover acts as an automated mathematical auditor, analyzing smart contract code and developer-defined rules to provide proof of correctness or counterexamples that reveal vulnerabilities. Unlike traditional audits and testing, formal verification guarantees security by detecting all possible bugs and proving their absence.

Certora's formal verification technology has already proven its effectiveness by identifying critical vulnerabilities in widely used protocols, such as a fundamental flaw in MakerDAO's DAI equation, a bug in SushiSwap's Trident pools, and an issue in PRBMath's rounding logic. These findings demonstrate the power of formal verification in uncovering vulnerabilities that may otherwise go undetected.

By open-sourcing the Prover, Certora invites developers, security researchers, and the broader Web3 community to join this effort. Developers can now integrate formal verification early in the development process, reducing audit costs and preventing exploits before they happen. The Prover supports multiple chains, allowing projects across Ethereum, Solana, and Stellar to benefit from automated, mathematically sound security