Certora Formal Verification

Write mathematical proofs that your smart contracts are correct for ALL possible inputs. Certora translates Solidity + CVL specifications into SMT formulas and exhaustively verifies them — no sampling, no random fuzzing, full coverage of the state space.

What You Probably Got Wrong

LLMs confuse CVL with Solidity, hallucinate syntax, and miss the fundamental workflow. Fix these blind spots first.

• CVL is NOT Solidity — It is a separate language (Certora Verification Language) with its own syntax, types, and semantics. You cannot use Solidity expressions like abi.encode or keccak256 in CVL. CVL has methods blocks, rule declarations, invariant, ghost, and hook — none of which exist in Solidity.
• Certora requires an API key — The Prover runs on Certora's cloud infrastructure. You need a CERTORAKEY environment variable. Academic and open-source projects get free access. Commercial pricing is per-verification-minute.
• Counter-examples are the key output — When a rule fails, Certora produces a concrete counter-example showing exact call sequences, storage values, and variable assignments that violate your property. Reading these is the core skill — writing specs is secondary.
• Verification is exhaustive, not sampling — Unlike fuzz testing (Foundry, Echidna) which tests random inputs, Certora proves properties hold for ALL possible inputs, ALL possible call sequences, and ALL possible storage states. A passing rule means no counter-example exists.
• satisfy is NOT assert — satisfy checks reachability (can this state be reached?). assert checks universality (does this always hold?). Confusing them produces vacuously passing specs.
• require in CVL constrains the prover, not the contract — A CVL require narrows the search space. Over-constraining with too many require statements makes rules vacuously true (they pass because no valid execution exists). Use rule_sanity to catch this.
• Loops need explicit bounds — The Prover unrolls loops. Without --loop_iter N in your config, loops default to 1 iteration. Most real contracts need 3-7. Too high and verification times explode.
• mathint is unbounded — CVL's mathint type has no overflow. Use it for arithmetic in specs to avoid reasoning about overflow in the spec itself (the contract still has its Solidity overflow behavior).
• Invariants use induction, not enumeration — Certora proves invariants by assuming they hold at state N and proving they hold at state N+1. The base case (constructor) is checked separately. A failing invariant often means your preserved block is missing assumptions.

Installation