Formal verification scoping checklist

Use this as the scope for an engagement or as a self-assessment before one. Items are grouped by the failure class they prevent.

Before engaging anyone

• A written specification exists: public and private inputs, encodings, field and integer ranges, and explicit assumptions. If it does not, the first deliverable is the specification.
• The target is chosen by consequence: a range check, hash gadget, instruction chip or verifier whose failure would matter, not the easiest component.
• Automatic tools have already run (Circomspect, Picus or CIVER, Kani or CBMC on the prover code) so proof effort goes to what they cannot answer.

Theorems to demand

• Soundness stated over the specification's domain, quantifying over every satisfying witness, not the honest witness generator.
• Completeness, or a written reason it is out of scope and a test suite covering the honest path.
• For multi-table or zkVM systems, a whole-system statement (Clean Channels, sp1-lean style), not only per-chip theorems.
• For proof systems, which components are covered (sum-check, FRI, Fiat-Shamir) and at what security level.

Trusted computing base

• The prover and version pinned (Lean toolchain, Mathlib commit); axioms listed; no native_decide or an explicit justification.
• The extraction or translation step named (Halva synthesis hook, LLZK, hax, Aeneas) and whether it is verified or trusted.
• A mapping from the verified model to the deployed constraints and verifier code, with the compiler, codegen and integration gaps listed.

Handover

• Proof sources in a repository with a single command that rechecks them in CI, and CI actually running it.
• A list of unproved obligations, sorries and trusted lemmas with owners and dates.
• A maintenance plan: what happens to the proofs when the circuit or specification changes.

Outside the proof

• An audit plan for the protocol layer, verifier integration, on-chain contract and deployment, since proofs cover none of these.
• Constant-time and side-channel review for any implementation-level work; functional correctness does not imply it.
• A reading of the theorem statements by someone who did not write them, specifically looking for assumptions that exclude real inputs (the SP1 JALR pattern).

Firms that can run this with you

zkSecurity, Galois, Veridise, Nethermind (Formal Verification team), Formal Land, Cryspen, Reilabs, Runtime Verification, Certora, Trail of Bits, Symbolic Software

Last reviewed 2026-09-13 by the sorryfree editors. Machine-readable: checklist.json · summary.txt