Formal verification scoping checklist for ZK circuits and cryptographic code
============================================================================

What to agree before a formal verification engagement and what to demand at handover: a written specification, the exact theorems (soundness and completeness), the trusted computing base, the link between the model and the shipped code, a CI recheck command, and an audit plan for everything outside the proof.

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).

Source page: https://sorryfree.com/checklist/
Compiled by: sorryfree editors (https://sorryfree.com/about/)
Last reviewed: 2026-09-13