We are open-sourcing the Certora Prover, the most advanced Formal Verification (FV) engine for Ethereum (EVM), Solana (sBPF), and Stellar (WASM). Secure your code with this industrial-grade tool, which is now free, transparent, and community-driven.

Discover the formally verified protocols using the Certora Prover in our Security Portfolio.

Why Open Sourcing Security Matters

Smart contract security is expensive and slow. DeFi projects spend over a year on development and millions on audits to ensure they don’t fall victim to catastrophic exploits. While critical bugs have become rarer, the high cost and complexity of securing smart contracts make DeFi an exclusive club—one that requires massive funding before a single line of code is deployed. 

This model isn’t sustainable. Security shouldn’t be a privilege reserved for the well-funded; it should be efficient, accessible, and integrated into the development process.

The Certora Prover has been developed for 7+ years and has secured a total of over $100 Billion in TVL across projects like Aave, MakerDAO, Uniswap, Lido, EigenLayer, Solana Foundation, Ether.fi, Silo, Safe, Kamino, Squads, Jito, Manifest, Balancer, Morpho, and many others. Developers have already written over 70,000 rules. Unlike auditing and testing, formal verification is the only method that guarantees security for all formalized rulesets by detecting all bugs and eventually proving their absence.

What is the Certora Prover?

Think of it as an “automated mathematical auditor" for smart contracts:

1. Inputs: Your contract’s code + rules (written in the Solidity-like and open-source Certora Verification Language (CVL).
2. Outputs: Proofs of correctness or counterexamples showing bugs.
3. Results: Guarantees that your code is secure and behaves as intended.

Example:
A rule can say that even a malicious user can never withdraw more assets than they have deposited and rightfully earned. The Prover checks all possible scenarios, not just a few test cases. This ensures that the protocol can never be hacked by a bug that allows a hacker to withdraw more assets than they deserve.

Real-World Impact: Bugs Caught by Certora Prover

1. MakerDAO’s DAI Equation Bug

• Issue: A core invariant—the "Fundamental Equation of DAI"—has been mathematically incorrect since 2018. It was not found in an audit by a top auditing firm, was incorrectly proven mathematically by the Maker team themselves, and was only found by the Certora Prover.
• Risk: Undermined the stability of one of crypto’s largest stablecoins.
• Outcome: Fixed pre-deployment, avoiding systemic risk.

2. SushiSwap’s Trident Pool Drain

• Issue: Broken invariant lets attackers drain liquidity pools.
• Risk: Loss of millions in user funds.
• Outcome: Patched before exploit.

3. PRBMath’s Rounding Error

• Issue: Wrong rounding direction in the signed mulDiv() function.
• Risk: Draining liquidity providers’ funds.
• Outcome: The bug was highlighted in the library’s documentation and will be fixed in the new version. 

4. Jito Restaking Re-staking Vault Reserve Calculation Bug

• Issue: The reserve amount in the vault is computed using the wrong units.
• Risk: The vault may over-delegate and not be able to cover all withdrawal requests.
• Outcome: Fixed pre-deployment before exploit.

5. Manifest Vault Transfer Bug

• Issue: For Token-2022, funds are transferred from the user to the vault on withdrawal instruction.
• Risk: Protocol drains user funds unexpectedly
• Outcome: Fixed pre-deployment before exploit.

Why Developers Love Certora

• Shift Left Security: Catch bugs early—like spellcheck for code.
• Audit Readiness: Reduce audit costs by 30% with pre-verified code.
• Multi-Chain: Supports Ethereum, Solana, and Stellar.
• Automated Security: Write it once and run it on every change.
• Security Guarantees: Have peace of mind of mathematical correctness.
• Compiler Bug Detection: Protects against subtle bugs introduced by compilers, as demonstrated by uncovering several bugs in the Solidity compiler (including silent corrupt storage, optimizer bug, bump allocator bug, incorrect calldata validation, memory isolation violation, and memory corruption) via static analysis.
• Free: The Certora Prover is now free and open-source.

Join the Formal Verification Security Movement

Formal verification isn’t just for PhDs anymore. With AI-generated code and composable DeFi, mathematical guarantees are non-negotiable. By open-sourcing the Prover, we’re empowering builders to:

✅ Prevent exploits before they happen.

✅ Build trust with verifiable correctness.

✅ Democratize security across Web3.

Follow us on Twitter and star us on GitHub

Security shouldn’t be a privilege—it’s a right. Make bulletproof smart contracts the norm.

• If you’re a developer: Sign up and start verifying today
• Security researchers: Join Certora's competitions to help secure leading DeFi projects, test your skills, and earn rewards.