certora-prover

A Claude Code / Agent Skill for writing CVL specs and formally verifying EVM smart contracts with the Certora Prover.

certora-prover is an Agent Skill that teaches Claude Code how to write CVL (Certora Verification Language) specifications and formally verify Solidity/EVM smart contracts with the Certora Prover. It packages condensed, task-oriented references, a one-page cheatsheet, and a fully worked ERC20 example so the agent can author rules, invariants, ghosts, hooks, and methods/summaries, run certoraRun against a .conf, and diagnose vacuity, soundness, and timeout problems — without you re-explaining CVL every session.

The whole point of formal verification is different from testing, and this skill keeps the agent honest about it:

• Prove, don't test. Unit tests and fuzzers sample a handful of inputs. The Prover reasons symbolically over every input, caller, and storage state your model allows — so a passing rule is a proof for all inputs, and a failing one yields a concrete counterexample (CEX) you can inspect.
• Sound but incomplete. Within the model the Prover won't miss a violation, but it can time out, and it only checks what your spec actually asserts. An empty or 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.

The skill is a single certora-prover/ directory: a SKILL.md entrypoint plus reference files Claude loads on demand.

Reference library (references/)

• cvl-language.md — CVL syntax and semantics: types, env, expressions, mathint, havoc, CVL functions, definitions, the methods block basics.
• rules-invariants.md — writing rules and invariants: parametric rules (method f), preserved blocks, inductive reasoning, assert vs satisfy.
• methods-and-summaries.md — the methods block in depth: envfree, exact vs wildcard entries, DISPATCHER, NONDET, ALWAYS, CONSTANT, function and ghost/expression summaries.
• hooks-and-ghosts.md — ghost variables/mappings, Sload/Sstore hooks, init_state, and tracking accounting properties like sumOfBalances == totalSupply.
• running-and-config.md — installing certora-cli, the CERTORAKEY, project layout, the .conf (JSON5) format, key flags, and reading the web report.
• spec-patterns-cookbook.md — reusable patterns: state-change isolation, integrity rules, revert-condition rules, additivity/commutativity, access control.
• soundness-and-approximations.md — what makes a proof sound or unsound: optimistic loops, summaries, require, harnessing, and the assumptions ledger.
• debugging-and-timeouts.md — diagnosing vacuity, taming timeouts, CEX call-trace reading, splitting rules, and performance levers.
• advanced-defi-patterns.md — vault/AMM/lending-style properties, multi-contract scenes, and cross-function invariants.
• tooling-and-ecosystem.md — the surrounding tooling: CLI, VS Code support, CI usage, and report artifacts.
• learning-resources.md — curated pointers to official docs, tutorials, and example repos for going deeper.

Quick lookup

• cheatsheet.md — a one-page lookup card of CVL constructs and certoraRun flags, each with a one-liner and a link to the deeper reference.

Worked ERC20 example (examples/)

• examples/ERC20.spec — a complete, realistic CVL spec for a standard ERC20: an envfree methods block, the totalSupplyIsSumOfBalances invariant, and rules covering state-change isolation, transfer integrity, revert conditions, transferFrom additivity, transfer commutativity, and mint access control.
• examples/ERC20.conf — a fully commented, runnable .conf (JSON5) explaining every flag (files, verify, solc, rule_sanity, optimistic_loop, loop_iter, multi_assert_check, packages, wait_for_results, …) so you can copy it as a starting template.

npx skills add zakrad/certora-prover-skill --skill certora-prover

Clone the repo and copy the skill into your Claude Code skills directory:

git clone https://github.com/zakrad/certora-prover-skill.git
cp -r certora-prover-skill/certora-prover ~/.claude/skills/

Prefer to scope it to a single project instead of installing it globally? Copy it into that project's .claude/skills/ directory:

cp -r certora-prover-skill/certora-prover .claude/skills/

(~/.claude/skills/ makes the skill available everywhere; a project-level .claude/skills/ keeps it local to that repo and lets you commit it alongside your contracts.)

However you install it, the skill auto-activates in Claude Code: whenever you start writing CVL, editing a .spec/.conf, or ask Claude to verify a contract, Claude detects the task and pulls in the relevant references automatically. No manual toggling required.

Once installed, just describe the verification task and the skill kicks in:

You: Write a CVL invariant proving totalSupply always equals the sum of all balances
     for my ERC20, then give me a .conf to run it.

Claude (certora-prover skill active):
  → drafts the ghost + hook to track the running sum of balances
  → writes `invariant totalSupplyIsSumOfBalances()` with a preserved block
  → emits an ERC20.conf with rule_sanity: basic and optimistic_loop set
  → tells you exactly which certoraRun command to run and how to read the report

# 1. Install the CLI and set your key
pip install certora-cli
export CERTORAKEY=<your-key-from-certora.com>

# 2. A tiny spec — certora/specs/Sanity.spec
cat > certora/specs/Sanity.spec <<'CVL'
methods { function totalSupply() external returns(uint256) envfree; }

rule totalSupplyNeverReverts {
    totalSupply@withrevert();
    assert !lastReverted, "totalSupply() should never revert";
}
CVL

# 3. Run it (conf-less form)
certoraRun src/MyToken.sol:MyToken \
    --verify MyToken:certora/specs/Sanity.spec \
    --rule_sanity basic --msg "sanity"

certoraRun compiles your contract, submits the job, and prints a report URL with per-rule PASS/FAIL and counterexample call traces. For the real spec and a fully commented config, copy examples/ERC20.spec and examples/ERC20.conf.

certora-prover-skill/
├── README.md
└── certora-prover/                       # the skill (this is what gets installed)
    ├── SKILL.md                          # entrypoint: mental model + workflow
    ├── cheatsheet.md                     # one-page CVL + certoraRun lookup card
    ├── references/
    │   ├── cvl-language.md
    │   ├── rules-invariants.md
    │   ├── methods-and-summaries.md
    │   ├── hooks-and-ghosts.md
    │   ├── running-and-config.md
    │   ├── spec-patterns-cookbook.md
    │   ├── soundness-and-approximations.md
    │   ├── debugging-and-timeouts.md
    │   ├── advanced-defi-patterns.md
    │   ├── tooling-and-ecosystem.md
    │   └── learning-resources.md
    └── examples/
        ├── ERC20.spec                    # complete worked ERC20 specification
        └── ERC20.conf                    # fully commented runnable config

This skill distills and reorganizes material from the official Certora documentation at docs.certora.com (CVL language reference, the Certora Prover user guide, and the published tutorials/examples) into a format optimized for an AI coding agent.

This is an UNOFFICIAL, community-maintained skill. It is not affiliated with, endorsed by, or supported by Certora. "Certora", "Certora Prover", and "CVL" are the property of their respective owners. For authoritative and up-to-date guidance, always defer to the official docs at docs.certora.com.

Contributions are welcome. If a reference is out of date with the current certora-cli, an example doesn't run, or you have a pattern worth adding:

1. Open an issue describing the change, or
2. Fork, edit the relevant file under certora-prover/, and open a pull request.

Please keep the same style: task-oriented, concise, and cross-linked, with runnable examples wherever possible.

MIT © contributors.

Formal verification provides strong guarantees, but those guarantees hold only modulo your assumptions — every require, summary, harness, loop bound, and optimistic flag narrows the model being checked, and the proof says nothing about behavior outside it. A passing run is not a substitute for audits, careful spec review, or your own judgment. This skill is provided "as is", without warranty of any kind; you are responsible for the specs you write and the conclusions you draw from them.