Formal Verification and Security Audits for Smart Contracts

Certora is an Israeli company founded in 2018 by a team out of Tel Aviv University, led by CEO Mooly Sagiv, who chairs software systems there, and CTO Shelly Grossman. It sells formal verification tooling and security review services to smart contract developers building on Ethereum, Solana, Stellar, and Sui. Its published customer list includes protocol teams such as Aave, Compound, MakerDAO, Lido, Balancer, and Morpho, and the company has raised roughly $43 million in funding.

The Certora Prover takes a contract plus a specification written in the company's rules language, then applies mathematical analysis to check that the rules hold across every possible contract state and execution path. When a rule can be violated the Prover returns a counterexample showing the exact sequence that breaks it, rather than a probabilistic finding. Teams wire the Prover into continuous integration so every commit is re-verified, turning verification into a recurring build step.

Alongside the Prover, Certora runs manual security audits staffed by formal verification specialists who write specifications with the client and consult interactively during the review, and it operates crowdsourced verification contests in partnership with platforms including Code4rena. Gambit, its mutation testing tool, generates mutants of contract code to measure whether a specification is strong enough to catch real bugs. The tooling spans several blockchain ecosystems rather than targeting a single chain.