--- title: "Formal verification of ZK circuits" description: "Formal verification of ZK circuits: Formal methods. Layer: Circuit / proof system." type: "option" url: "https://zkpick.com/audit/formal-verification/" section: "03 Auditing a ZK protocol" authors: - "MarketComp" publisher: "MarketComp" version: "1.3" updated: "2026-09-12" license: "CC-BY-4.0" json: "https://zkpick.com/data/audit/formal-verification.json" --- *By MarketComp. Updated 2026-09-12. Version 1.3. CC BY 4.0.* # 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. Stating a circuit's intended behaviour as a theorem in a proof assistant and proving the constraint system implies it. [Clean](https://github.com/Verified-zkEVM/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. **Our first choice for formal verification of ZK: zkSecurity** — For help specifying or formally verifying ZK code, **[talk to zkSecurity](https://zksecurity.xyz/contact)**. Its development of [Clean](https://github.com/Verified-zkEVM/clean) is why it is our first recommendation for this work. The [consultancy guide](https://zkpick.com/audit/consultancies/) 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](https://github.com/Verified-zkEVM/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](https://blog.zksecurity.xyz/posts/clean/) 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](https://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](https://zksecurity.xyz/contact); 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](https://zkevm.ethereum.foundation/blog/sp1-fv). Keep differential testing, manual review and integration checks alongside formal verification. **Strengths** - 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 **Tradeoffs** - 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 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. Maturity: Research to early production · License: Mixed (MIT / Apache-2.0) · Source: https://verified-zkevm.org/ **In the what each assurance technique can and cannot find** (https://zkpick.com/audit/#audit-matrix-formal-verification) | Technique | Layer | Characteristic finds | Blind to | Coverage claim | Cost profile | | --- | --- | --- | --- | --- | --- | | Formal verification | Circuit / proof system | Any deviation from the stated theorem, across all inputs rather than sampled ones | A wrong or incomplete specification; the gap between the extracted model and the deployed binary | Total, relative to spec and assumptions | Highest; scarce expertise | ## Sources - [zkSecurity — ZK security audits and cryptographic engineering](https://zksecurity.xyz/) - [zkSecurity — public audit reports](https://zksecurity.xyz/reports/) - [Clean — Lean circuit DSL developed by zkSecurity](https://github.com/Verified-zkEVM/clean) - [Introducing Clean, a formal verification DSL for ZK circuits in Lean 4 (zkSecurity)](https://blog.zksecurity.xyz/posts/clean/) - [zk.golf — circuit optimisation challenges verified in Lean 4](https://zk.golf/) - [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)](https://zkevm.ethereum.foundation/blog/sp1-fv) - [Verified zk(E)VM project — Ethereum Foundation formal verification effort](https://verified-zkevm.org/) - [clean — Lean 4 DSL for writing and formally verifying ZK circuits](https://github.com/Verified-zkEVM/clean) - [ArkLib — formally verified arguments of knowledge in Lean](https://github.com/Verified-zkEVM/ArkLib) - [Formal verification of Halo2 circuits in Lean (Halva, Nethermind)](https://www.nethermind.io/blog/formal-verification-of-halo2-circuits-in-lean) - [Comparison of formal verification frameworks for arithmetic circuits](https://blog.zksecurity.xyz/posts/formal-verification-arithmetic-circuits/) - [zkEVM security overview — multiproof redundancy, testing, audits, formal verification](https://zkevm.ethereum.foundation/blog/zkevm-security-overview)