zakrad/certora-prover-skill

Certora Prover (CVL / EVM)

The Certora Prover formally verifies smart contracts: you write specs in CVL (Certora Verification Language) describing properties (rules and invariants), and the Prover either proves them for all inputs and states or returns a concrete counterexample (CEX).

Core mental model — read this first:

• Prove, don't test. Unlike unit tests or fuzzing (which sample a few inputs), the Prover reasons symbolically over every input, caller, and storage state allowed by your model.
• Sound but incomplete. Within the model it won't miss a violation, but it can time out, and it only checks what your spec actually asserts. An empty/weak spec proves nothing useful.
• "Verified" = no counterexample within the model, modulo your assumptions. Every require, summary, loop unroll, and optimistic flag narrows the model. A green checkmark is only as strong as those assumptions — getting them right is the whole game.

Workflow: verifying an app from scratch

1. Install + key. pip install certora-cli; set CERTORAKEY. (→ references/running-and-config.md)
2. Project layout. Put contracts under src/, specs under certora/specs/, a .conf per target. (→ references/running-and-config.md)
3. Write a first sanity/parametric rule. Start tiny: a parametric rule (method f) asserting some basic property holds after any function, just to confirm the harness compiles and runs. (→ references/rules-invariants.md, references/spec-patterns-cookbook.md)
4. Run it. certoraRun MyContract.conf (or pass the .sol/.spec directly), then open the report link. (→ references/running-and-config.md)
5. Read the report. Inspect CEX call traces and storage; fix the spec or confirm a real bug. (→ references/running-and-config.md, references/debugging-and-timeouts.md)
6. Add invariants + ghosts. State the real properties: inductive invariants, plus ghosts/hooks for accounting (e.g. sumOfBalances == totalSupply). (→ references/rules-invariants.md, references/hooks-and-ghosts.md)
7. Harden soundness + sanity. Always run --rule_sanity basic; review every summary and assumption; remove or justify any unsound shortcut. (→ references/soundness-and-approximations.md, references/methods-and-summaries.md)
8. Mutation-test. Use Gambit to confirm your rules actually catch injected bugs — a spec that survives mutants is over-assuming. (→ references/debugging-and-timeouts.md)

10-second QUICKSTART

pip install certora-cli
export CERTORAKEY=<your-key>

// Counter.spec — prove increment() strictly increases the value
methods {
    function get() external returns (uint256) envfree;
}

rule incrementIncreases(env e) {
    uint256 before = get();
    increment(e);
    assert get() > before, "increment must increase the counter";
}

certoraRun src/Counter.sol:Counter \
    --verify Counter:certora/specs/Counter.spec \
    --solc solc8.20 \
    --rule_sanity basic \
    --msg "counter increment"

How to use this skill / reference map

Read the file that matches the task in front of you:

• references/cvl-language.md — read when you need CVL syntax: file structure, types (mathint/env/method/calldataarg/storage), casts and their soundness, operators/quantifiers, require vs assert vs satisfy vs havoc, functions vs definitions, and how to call contract methods (env, envfree, withrevert, lastReverted).
• references/rules-invariants.md — read when writing rules, parametric rules (method f), satisfy witnesses, or inductive invariants with preserved blocks and requireInvariant.
• references/methods-and-summaries.md — read when wiring up the methods block: entry kinds, envfree/optional, the full summary catalogue + soundness table, expression/ghost summaries, and multi-contract setups (using, links, DISPATCHER).
• references/hooks-and-ghosts.md — read when you need to mirror storage or prove accounting: storage/opcode/transient hooks, ghost vars/functions, sum ghosts, and persistent ghosts.
• references/running-and-config.md — read when installing, running certoraRun, writing .conf files, choosing flags, laying out a project, or interpreting the web report.
• references/spec-patterns-cookbook.md — read when you want a ready recipe: access control, "what can change", sum-of-balances, monotonicity, frame conditions, state machines, round-trips, commutativity, revert conditions, and unit-test-style rules.
• references/advanced-defi-patterns.md — read when verifying a real protocol and the basic cookbook isn't enough: ERC4626 vault exchange-rate monotonicity (cross-multiplication, no-free-lunch, preview bounds), AMM k-invariant & no-value-extraction, lending solvency/health/"no bad debt" & anti-lockup liveness, reward-drift accounting, reentrancy-as-CEI, and role-based access control at scale — each idiom attributed to the production repo (Morpho/OZ/Aave/Certora) it comes from.
• references/tooling-and-ecosystem.md — read when wiring Certora into CI (GitHub Actions, caching, gating PRs) or deciding which tool fits a property: a Certora vs Halmos vs Foundry (invariant/fuzz) vs Echidna decision guide, with when-to-reach-for-each tradeoffs.
• references/learning-resources.md — read when you want to go deeper or onboard: curated external links — RareSkills/Certora tutorials, official docs, talks, and real-world public spec repos (Morpho, Aave, OpenZeppelin, Compound) worth reading as worked examples.
• references/soundness-and-approximations.md — read when deciding what to assume vs assert: sound/pessimistic vs unsound/optimistic, loop/hashing/havoc approximations, the optimistic-flag family, what a passing rule guarantees, and the soundness review checklist.
• references/debugging-and-timeouts.md — read when a rule is vacuous, slow, or suspicious: --rule_sanity, timeout mitigation (summaries, splitting, range constraints), the TAC difficulty report, Gambit mutation testing, the VSCode LSP, and the "should I trust this pass?" checklist.
• cheatsheet.md — read when you want a one-page quick reference: the most-used CVL keywords, rule/invariant skeletons, common certoraRun flags, and the top footguns at a glance.
• examples/ERC20.spec — read when you want a complete worked spec: methods block, sum-of-balances ghost+hook, supply invariant, parametric/integrity/revert/additivity rules, and mint access control.
• examples/ERC20.conf — read when you need a runnable JSON5 conf template covering every common key (files, verify, solc, packages, optimistic_loop, rule_sanity, ...).

Golden rules / common footguns

• require ≠ revert. require assumes a fact (prunes the model); it does not check a contract revert. To reason about reverts use withrevert + lastReverted.
• Watch vacuity. An over-constrained require can make a rule pass trivially because no input survives. Always run --rule_sanity basic (prefer advanced).
• Optimistic flags are unsound. --optimistic_loop, --optimistic_hashing, --optimistic_fallback, etc. assume away cases. Use them deliberately, document why, and prefer eliminating the need.
• Prefer preserved over filtered. For invariants, encode assumptions in preserved blocks (with requireInvariant) rather than silently excluding methods.
• Use mathint for accumulators. Sums and counters in uint256 can overflow and produce phantom CEXs (or hide real ones); compute in unbounded mathint, cast at the boundary.
• A passing rule is only as good as its assumptions. Every summary, link, loop bound, and require is a hole in the proof. Mutation-test to confirm the rule can actually fail.

---

Most-used files: start from references/spec-patterns-cookbook.md for the right recipe and examples/ERC20.spec for a full working spec to adapt.