Industry-standard formal verification platform for EVM, Solana, and Stellar smart contracts. Specs are written in CVL (Certora Verification Language); the prover compiles contracts to math and exhaustively checks rules using SMT solvers on Certora's cloud.
- 01high-assurance proofs of critical invariants
- 02ERC-20/4626/4337 conformance specs
- 03rule-based verification of access control and accounting
- 04regression of historical exploits as parametric rules
- 05compliance evidence for audited protocols
- pipx install certora-cli
- # Then export your API key: export CERTORAKEY=<your-key-from-certora.com>
- # Requires Java 11+ and solc on PATH
| Variable | Scope | Description |
|---|---|---|
| CERTORAKEY | Server | Personal access key obtained from certora.com. Required for `certoraRun` to dispatch jobs to Certora's cloud prover. |
Use Certora for formal verification of safety-critical rules. Write a `.spec` file in CVL: `rule transferPreservesTotalSupply(address to, uint256 amount) { uint256 before = totalSupply(); transfer(to, amount); assert totalSupply() == before; }` and dispatch with `certoraRun src/Token.sol --verify Token:specs/Token.spec --solc solc8.28 --msg "Token rules v1"`. Use `--rule <name>` to scope a single rule, `--optimistic_loop` for bounded loops, and `methods { ... }` blocks in the spec to summarize external calls. Configure runs via `certora.conf` JSON, then `certoraRun certora.conf`. Results stream to a job URL on prover.certora.com with counterexample traces.
- ⚑CVL rules over-trust `methods { ... }` summaries — if you mark an external as `envfree` or `NONDET` incorrectly, the prover happily proves false rules; treat summaries as untrusted assumptions.
- ⚑Loop unrolling defaults to depth 1 with `--loop_iter` — under-bounded loops produce vacuous proofs; pair `--optimistic_loop` only with explicit `require` bounds.
- ⚑Storage-slot collisions in upgradeable contracts confuse the prover; use `--prover_args '-enableStorageAnalysis true'` and verify the resolved layout in the job report.
- ⚑Each run consumes prover credits/time and counterexamples may be SMT timeouts (UNKNOWN) rather than true UNSAT — gate CI on `SAT`/`UNSAT` only and re-run flaky rules with longer `--smt_timeout`.
- ⚑CVL is not Solidity — `address(0)` ghost values and unconstrained `env` fields routinely produce counterexamples that are infeasible on-chain; constrain with `requireInvariant` and `env e`.