Certora Prover

Open Source

Certora Prover checks smart-contract bytecode against rules you write in the Certora Verification Language (CVL). Use it when you need an SMT-backed check that those rules hold on the modeled executions, with a concrete counterexample trace when an assertion fails.

About

Certora's user guide describes the Prover as compiling a contract and a CVL specification into verification conditions that an SMT solver proves or disproves. Rules and invariants call into the contract and assert expected behavior; a failed rule is returned as a concrete example. CVL syntax is close to Solidity, with extra features for writing specifications. The Prover was open-sourced on 2025-02-24 under GPL-3.0; the hosted cloud platform and audits are Certora's commercial offering. Targets are EVM bytecode, Solana (sBPF), and Stellar (WASM). The product page lists Aave and Compound among its users.