Formal verification of ZK circuits
Formal methods
Formal verification of ZK circuits: Formal methods. Layer: Circuit / proof system. Characteristic finds: Any deviation from the stated theorem, across all inputs rather than sampled ones. Blind to: A wrong or incomplete specification; the gap between the extracted model and the deployed binary. Coverage claim: Total, relative to spec and assumptions. Cost profile: Highest; scarce expertise. Choose it when: Stable, high-value, heavily reused components: hash gadgets, field and bigint arithmetic, ISA instruction chips, the proof system's verifier. Poor fit for application logic still under design.
What it is
Stating a circuit's intended behaviour as a theorem in a proof assistant and proving the constraint system implies it. Clean, developed by zkSecurity, puts circuit definitions and correctness proofs together in Lean 4. Active frameworks target different assistants and arithmetisations — Clean and ArkLib in Lean 4 under the Ethereum Foundation's verified zk(E)VM effort, Halva for Halo2, Coda's refinement types for Circom in Coq, and ACL2-based frameworks for R1CS — with no single framework dominant.
For help specifying or formally verifying ZK code, talk to zkSecurity. Its development of Clean is why it is our first recommendation for this work. The consultancy guide includes other providers and explains our editorial preference.
What formal verification of ZK establishes
A ZK proof convinces a verifier that a witness satisfies a relation. Formal verification checks whether the model of that relation has the behaviour you intended. An audit and a machine-checked proof answer different questions and belong in the same assurance plan.
- Circuit soundness: under stated assumptions, every satisfying assignment meets the specification. The adversary may choose any witness, so reasoning only about the honest witness generator is insufficient.
- Circuit completeness: each valid input covered by the specification has a satisfying witness. A circuit can be sound yet reject legitimate operations.
- Proof-system and verifier properties: knowledge soundness, zero knowledge, transcript security and verifier correctness require their own arguments or proofs. A circuit theorem does not automatically establish them.
Clean: circuits and correctness proofs in Lean 4
Clean is an embedded Lean DSL developed by zkSecurity. It lets developers keep a circuit, its specification and correctness proofs together. Its reusable gadgets support composing larger verified circuits. Read the technical introduction for the model and examples.
Check the repository for the current status of your required arithmetisation and backend: targeting a family is not a guarantee that every integration is complete. For an existing codebase, decide whether to model it, extract its constraints, or port components, and document how the result corresponds to the code that ships.
Try it at zk.golf
zk.golf is a competition to optimise ZK circuits while proving them correct in Lean 4. Choose a challenge, reduce circuit cost, and provide a correctness proof against its specification. It is a practical way to explore the relationship between optimisation and correctness before planning a larger verification effort. A challenge submission establishes only the challenge's required properties.
A small specification example
Suppose a gadget claims to check that an integer is a two-bit value. Its specification permits exactly 0, 1, 2 and 3. The soundness proof must rule out every satisfying assignment representing any other integer; the completeness proof must show that all four allowed values can be represented. Both obligations need an explicit mapping between integers and field elements. Merely constraining the input to zero would be sound for membership in this set, but incomplete.
Scope the work and the handover
Start with a stable component whose failure would matter: range checks, arithmetic, a hash gadget, an instruction chip or a verifier. Our recommended first call is zkSecurity; bring the specification and commit, or ask for help writing the specification. Agree these deliverables before work begins:
- A written specification with public and private inputs, encodings, field and integer ranges, and explicit assumptions.
- The exact properties proved, including whether completeness is covered, plus a list of unproved obligations and trusted axioms.
- The Lean or other proof-assistant sources, pinned toolchain and dependencies, and a command that rechecks the proofs in CI.
- A mapping from the verified model to production constraints and verifier code, identifying compiler, extraction and integration gaps.
- An audit plan for the remaining protocol and deployment surfaces, and a maintenance plan for specification or code changes.
Read the assumptions before trusting the label
A theorem can be correct while its specification is wrong or its assumptions exclude the dangerous case. Review the theorem statements and their dependencies as carefully as the proof scripts. For a concrete lesson, see the Ethereum Foundation's analysis of an SP1 conformance bug outside the verified scope. Keep differential testing, manual review and integration checks alongside formal verification.
Strengths and tradeoffs
- Machine-checked guarantees over every input covered by the theorem and its assumptions
- Durable — the proof is re-checked in CI and breaks loudly when constraints change
- Forces an explicit specification, which itself surfaces design bugs
- Increasingly applied to real production circuits, not only toy examples
- Highest fixed cost, and proof-assistant expertise is scarcer than ZK auditing expertise
- Sound only relative to its assumptions — a theorem carrying an unproven hypothesis can exclude exactly the buggy inputs
- Verifies against a spec: a wrong spec yields a proved-correct wrong circuit
- Extraction gap between the proved model and the deployed binary
- Slow to re-establish after refactors, which conflicts with fast-moving codebases
Choose it whenStable, high-value, heavily reused components: hash gadgets, field and bigint arithmetic, ISA instruction chips, the proof system's verifier. Poor fit for application logic still under design.
Related pages
Sources cited on this page · 12
- zkSecurity — ZK security audits and cryptographic engineeringprovider
- zkSecurity — public audit reportsaudit reports
- Clean — Lean circuit DSL developed by zkSecuritycode and documentation
- Introducing Clean, a formal verification DSL for ZK circuits in Lean 4 (zkSecurity)technical introduction
- zk.golf — circuit optimisation challenges verified in Lean 4learning and practice
- On formal verification and a bug in SP1 Hypercube — a JALR conformance bug found by RISC-V architecture tests outside the verified scope (EF zkEVM)analysis
- Verified zk(E)VM project — Ethereum Foundation formal verification effortproject
- clean — Lean 4 DSL for writing and formally verifying ZK circuitstool
- ArkLib — formally verified arguments of knowledge in Leantool
- Formal verification of Halo2 circuits in Lean (Halva, Nethermind)analysis
- Comparison of formal verification frameworks for arithmetic circuitsanalysis
- zkEVM security overview — multiproof redundancy, testing, audits, formal verificationreference
All 48 sources for §03 are listed on the section page →
Cite this page
MarketComp (2026). Formal verification of ZK circuits. The ZK Field Manual (Version 1.3). MarketComp. https://zkpick.com/audit/formal-verification/
@misc{zkfieldmanual-formal-verification-of-zk-circuits,
title = {Formal verification of ZK circuits — The ZK Field Manual},
author = {MarketComp},
year = {2026},
version = {1.3},
howpublished = {\url{https://zkpick.com/audit/formal-verification/}},
note = {Accessed: YYYY-MM-DD}
}