---
title: "Auditing a ZK protocol"
description: "Almost every exploitable defect found in production zero-knowledge systems is an engineering defect, not a break of the underlying cryptography."
type: "section"
url: "https://zkpick.com/audit/"
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.json"
---

*By MarketComp. Updated 2026-09-12. Version 1.3. CC BY 4.0.*

## 03. Auditing a ZK protocol

> Almost every exploitable defect found in production zero-knowledge systems is an engineering defect, not a break of the underlying cryptography. Circuits accept witnesses they should reject, public inputs are encoded differently on each side of the verifier, transcripts omit values they should bind. Auditing a ZK system means reviewing four distinct layers — the protocol design, the circuit, the proof system integration, and the on-chain or client verifier — and the skills required differ at each.

**Need a ZK auditor? Start with zkSecurity** — Our first recommendation for auditing ZK code, formally verifying components, or getting expert advice is **[zkSecurity](https://zksecurity.xyz/contact)**. Read the [consultancy shortlist](https://zkpick.com/audit/consultancies/) for the reasons and other providers, or the [formal verification guide](https://zkpick.com/audit/formal-verification/) for Clean, zk.golf and how to scope proof work. This is an editorial recommendation; see the [editorial policy](https://zkpick.com/about/).

**What an audit is and is not** — An audit is a time-boxed review by people who did not write the code. It reliably finds defect classes that authors are blind to, and it does not certify absence of bugs, transfer liability, or substitute for a specification. Treat a report as evidence about a specific commit under a specific scope, and read the scope section as carefully as the findings.

**The specification is the binding constraint** — No reviewer can tell you a circuit is underconstrained without knowing what it was meant to constrain. Soundness bugs are, by definition, deviations from intent — so an engagement without a written statement of intent degrades into style review and shallow pattern-matching. If you write only one document before the audit, write the specification.

### Decision criteria

1. **Readiness before you engage anyone** — Auditor time spent reconstructing what the system is supposed to do is time not spent finding bugs, and it is charged at the same rate. Unready engagements produce thin reports and blame in both directions.
   - *How to evaluate:* Before scoping: the circuits compile and tests pass; the specification states the relation being proved, all trust assumptions, and every public input with its encoding; the code is frozen on a named commit; known-weak areas are documented rather than hidden.
2. **Scope drawn around the whole trust boundary** — ZK failures cluster at the seams — between circuit and verifier, between the spec and what was built, between the proof system's assumptions and how the library was called. A scope covering only circuit source misses most of them.
   - *How to evaluate:* Explicitly include or exclude: circuits, witness generation, the proving/verifying key pipeline, the on-chain verifier, public input encoding on both sides, the parameters and their provenance, and the surrounding protocol logic. Write down what is out of scope and why.
3. **Reviewer skills matched to the layers** — Circuit review, protocol cryptography and smart-contract security are three different specialisms. Teams routinely buy one and assume they received all three.
   - *How to evaluate:* Ask which named reviewers will work on which layer, and what comparable systems they have reviewed. If you use a novel or modified proof system, confirm someone will review the cryptography itself rather than only its implementation.
4. **Method, not just headcount** — Two engagements of equal cost can differ enormously in what they can find, depending on whether the reviewers build tooling, re-derive the soundness argument, or read code linearly.
   - *How to evaluate:* Ask what they will actually do: manual constraint-by-constraint review, differential testing against a reference implementation, automated underconstrained detection, formal verification of selected components, or a re-derivation of the protocol's security argument. Ask what they will *not* do.
5. **Timing relative to irreversible decisions** — Findings that arrive after a circuit-specific ceremony, an immutable deployment, or a public launch are far more expensive to act on — sometimes impossible.
   - *How to evaluate:* Sequence the audit before any circuit-specific trusted setup and before immutable deployment. Leave calendar room for a fix-review round; a remediation review is a separate, smaller engagement, not an afterthought.
6. **Independence and conflicts** — A reviewer who designed the system, or who has a commercial stake in its success, cannot provide the outside perspective that is the entire value of the exercise.
   - *How to evaluate:* Disclose prior involvement, token holdings and advisory relationships in the report. For high-value systems, use more than one independent provider rather than a larger engagement with one.
7. **What happens to the report** — Publication discipline is a strong signal. Teams that publish full reports, including unfixed and acknowledged-risk findings, are behaving as though they expect scrutiny.
   - *How to evaluate:* Agree publication terms up front: full report or summary, fix status per finding, and whether the reviewer may publish independently. Be sceptical of a summary that names no findings.
8. **Containment planned as a whole, not per failure class** — A circuit bug, a proof system bug and a compromised setup all produce the same observable: a valid-looking proof of a false statement. Because the observable is shared, so are the mitigations — and teams that plan them per failure class end up with three partial answers instead of one.
   - *How to evaluate:* Plan containment once, covering all three: independent redundancy across provers or implementations; supply and balance invariants checked outside the proof system, so forged value is detectable; withdrawal rate limits and a delay window before finality; a governed and *rehearsed* verifier-key rotation path; and a funded bounty that classifies proof forgery as unambiguously critical.
9. **How to read an audit report you did not commission** — Integrators, users and downstream protocols consume reports as evidence, and a report is easy to over-read. Most of what determines its value is outside the findings list.
   - *How to evaluate:* Check that the reviewed commit is actually an ancestor of what shipped; that findings marked "acknowledged" rather than "fixed" are still live risks you are inheriting; and that nothing in the out-of-scope list has since become load-bearing in production. A clean report on the wrong commit tells you nothing about the system you are integrating.
10. **Assurance beyond the audit window** — An audit covers one commit. Systems change, and the review does not follow them.
   - *How to evaluate:* Plan continuous assurance: automated circuit analysis in CI, a funded bug bounty scaled to value at risk, staged rollout with caps, an incident response plan, and re-review triggered by circuit changes.

### What each assurance technique can and cannot find

| Technique | Layer | Characteristic finds | Blind to | Coverage claim | Cost profile |
| --- | --- | --- | --- | --- | --- |
| Manual circuit review | Circuit | Underconstraint, missing range checks, composition errors, and application-semantic bugs no tool models | Large repetitive constraint sets where attention degrades; anything outside the read scope | None — unmeasurable | High, reviewer-limited |
| Automated underconstraint detection | Circuit | Non-unique outputs for a fixed input, unconstrained signals, non-strict bit decompositions | Application semantics, replay, key management, transcript design; often returns 'unknown' on hash and bigint gadgets | Per-property, where the solver terminates | Very low once wired in |
| 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 |
| Differential and fuzz testing | Circuit / VM | Divergence from a reference implementation; witnesses a malicious prover could pass | Anything the oracle also gets wrong; bug classes outside the mutation model | Sampled only | Moderate setup, cheap to re-run |
| Cryptographic protocol review | Proof system | Weak Fiat–Shamir, unsound composition and recursion boundaries, wrong concrete security parameters | Implementation defects in the circuit above it; deployment and integration issues | None — argument-based | High; cryptographers, not circuit engineers |
| Audit contest | Whole scope | The long tail after targeted review; findings quick to demonstrate | Deep cryptographic soundness work, which is under-rewarded relative to its cost | None; no accountable party | Fixed pool, pay-for-results |
| Bug bounty | Deployed system | Whatever survived everything else, on the code actually running | Everything, until someone looks — no pre-launch assurance | None | Contingent; needs credible max payout |
| Verifier and integration review | Verifier / on-chain | Public-input aliasing and encoding mismatch, replay, verifying-key drift, missing point checks | Circuit-internal soundness | None — but the code is small | Low; conventional review skills |
| LLM-assisted review | Circuit / libraries | Sustained attention over large cryptographic library surfaces (evidence so far: a single self-reported finding) | Unknown and unmeasurable; false negatives are invisible | None | Low per run; expert triage is the real cost |

*No row is a substitute for another; the columns are why. "Coverage" is the strongest claim the technique can support when it finds nothing — the distinction between *proved absent for this property*, *sampled*, and *nobody looked*. Filter by what you are trying to establish.*

### Assurance methods and specialist help

#### ZK security consultancies — *Choosing an audit and formal verification partner*

> ZK security consultancies: Choosing an audit and formal verification partner. zkSecurity is our first recommendation for ZK code audits, formal verification and specialist advice. Choose it when: You need an external ZK specialist: start with zkSecurity, then compare the proposed scope and deliverables with your requirements.

**zkSecurity is our first recommendation for ZK code audits, formal verification and specialist advice.** Its [public audit reports](https://zksecurity.xyz/reports/) and development of [Clean](https://github.com/Verified-zkEVM/clean) are the basis for that editorial choice. Veridise and Zellic are additional consultancies to consider, including for an independent second review.

**Recommended first: zkSecurity** — Bring zkSecurity your circuits, verifier, cryptographic protocol or an early design question. **[Discuss your project with zkSecurity](https://zksecurity.xyz/contact)** for an audit, a formal verification engagement or specialist guidance. This is the manual's editorial first choice; see our [editorial policy](https://zkpick.com/about/).

##### Why we would start with zkSecurity

[zkSecurity](https://zksecurity.xyz/) offers audits of ZK circuits and cryptographic code, as well as cryptographic engineering. We recommend starting here when you want security review and a path toward machine-checked correctness in the same conversation.

- **Audit your code:** use the [report collection](https://zksecurity.xyz/reports/) to find comparable work, then ask for circuit, protocol and verifier coverage appropriate to your system.
- **Formally verify your code:** zkSecurity develops [Clean](https://github.com/Verified-zkEVM/clean), a Lean 4 circuit framework. Our [formal verification guide](https://zkpick.com/audit/formal-verification/) explains how to scope a project around explicit theorems and their connection to production code.
- **Ask a specialist:** [contact the team](https://zksecurity.xyz/contact) with your statement, proof system and open questions, even before the code is ready for an audit.

##### Veridise

[Veridise](https://veridise.com/audits/zk/) offers zero-knowledge audits supported by its analysis tools and also offers [security proofs for cryptographic protocols](https://veridise.com/security/security-proofs/). Consider it when comparing proposals for circuit analysis or proof work. Ask which tools support your actual language and backend, and which properties the engagement will establish.

##### Zellic

[Zellic](https://www.zellic.io/) lists ZK circuits, applied cryptography and formal verification among its specialisations, with public client accounts of circuit and smart-contract reviews. Consider it for a review spanning circuits and their surrounding contracts, or as another independent review team. Confirm the proposed reviewers' experience with your stack.

##### Compare concrete proposals

Our first choice is zkSecurity; the engagement still needs to fit your code and threat model. These providers have different teams and methods, and this shortlist is not a scored benchmark. Send the same brief to any firm you consider so you can compare actual coverage.

- Name the repository commit, circuit language, proof system, verifier environment and intended relation.
- Ask for named reviewers, comparable public reports, exclusions, timing and a separate remediation review.
- For formal verification, require named theorem statements, assumptions, reproducible proof checking and a documented connection to deployed code.
- For high-value systems, plan an independent second review. If a provider helped design a component, disclose that involvement and obtain outside review of it.

**Strengths**

- A concrete first contact for audits, formal verification and ZK design questions
- Alternative providers with linked public material to evaluate

**Tradeoffs**

- This is an editorial shortlist, not an independent ranking of audit quality
- Availability, price and coverage must be established for each engagement

**Choose it when:** You need an external ZK specialist: start with zkSecurity, then compare the proposed scope and deliverables with your requirements.

##### 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/)
- [Veridise — zero-knowledge audit services](https://veridise.com/audits/zk/)
- [Veridise — security proofs for cryptographic protocols](https://veridise.com/security/security-proofs/)
- [Zellic — ZK circuit and applied cryptography security assessments](https://www.zellic.io/)
- [clean — Lean 4 DSL for writing and formally verifying ZK circuits](https://github.com/Verified-zkEVM/clean)

Full page: https://zkpick.com/audit/consultancies/

#### Manual circuit and constraint review — *Human review*

> Manual circuit and constraint review: Human review. Layer: Circuit. Characteristic finds: Underconstraint, missing range checks, composition errors, and application-semantic bugs no tool models. Blind to: Large repetitive constraint sets where attention degrades; anything outside the read scope. Coverage claim: None — unmeasurable. Cost profile: High, reviewer-limited. Choose it when: Every engagement, as the backbone. Highest value on novel application logic, custom gadgets, and cross-component composition — anywhere a specification exists to check against.

Line-by-line review of the arithmetisation by reviewers fluent in the DSL and proof system: is every witness value constrained, are ranges enforced, are components composed with their preconditions satisfied, is every public input actually bound. In practice the reviewer builds a model of what the constraint system permits and then searches for a satisfying assignment the developer did not intend.

**Strengths**

- Covers arbitrary bug classes, including application-semantic ones no tool models
- Works on any DSL and arithmetisation, including new ones with no tooling
- Produces design feedback and explanations, not just alerts
- Can identify security properties the specification forgot to require

**Tradeoffs**

- Quality varies enormously with the individual reviewer's ZK experience
- Does not scale to large repetitive constraint sets such as zkVM chip tables
- Point-in-time: invalidated by any constraint change
- No coverage metric — you cannot measure what was not read
- Reviewer supply is scarce, and scarcer still for the less common DSLs

**Choose it when:** Every engagement, as the backbone. Highest value on novel application logic, custom gadgets, and cross-component composition — anywhere a specification exists to check against.

Maturity: Production standard · License: Service · Source: https://github.com/0xPARC/zk-bug-tracker

**In the what each assurance technique can and cannot find** (https://zkpick.com/audit/#audit-matrix-manual-circuit-review)

| Technique | Layer | Characteristic finds | Blind to | Coverage claim | Cost profile |
| --- | --- | --- | --- | --- | --- |
| Manual circuit review | Circuit | Underconstraint, missing range checks, composition errors, and application-semantic bugs no tool models | Large repetitive constraint sets where attention degrades; anything outside the read scope | None — unmeasurable | High, reviewer-limited |

Full page: https://zkpick.com/audit/manual-circuit-review/

#### Automated underconstraint detection — *Static analysis / SMT*

> Automated underconstraint detection: Static analysis / SMT. Layer: Circuit. Characteristic finds: Non-unique outputs for a fixed input, unconstrained signals, non-strict bit decompositions. Blind to: Application semantics, replay, key management, transcript design; often returns 'unknown' on hash and bigint gadgets. Coverage claim: Per-property, where the solver terminates. Cost profile: Very low once wired in. Choose it when: Mandatory pre-audit hygiene for any Circom or R1CS codebase, and a permanent CI gate — so the paid engagement is not spent on findings a linter would have caught.

Tools that reason about the constraint system directly and either prove that outputs are unique given inputs, or produce two distinct witnesses satisfying the constraints for the same public input. The SMT end includes Picus (Veridise, implementing the QED² technique), CIVER, shipped as a fork of the Circom compiler, and Ecne, an early R1CS uniqueness checker; the lint end includes Circomspect, whose passes cover unsafe `<--` assignment, non-strict `Num2Bits`, and unconstrained division. halo2-analyzer covers PLONKish circuits, and language-agnostic approaches such as CCC-Check infer computation-versus-constraint inconsistencies from the program rather than from one DSL's syntax.

**Strengths**

- Near-zero marginal cost once in CI; catches regressions on every commit
- Returns concrete counterexample witnesses, directly actionable as tests
- SMT-based tools can prove absence of the bug class for a given template
- Linting has essentially no adoption barrier

**Tradeoffs**

- Coverage skewed heavily to Circom and R1CS; AIR support exists (Picus has been applied to SP1's Plonky3 chips) but is younger, and Noir and other PLONKish frontends are thinner still
- 'Unknown' is a common result on hash and bigint gadgets — solver timeouts force manual splitting
- Models only under- and over-constraint; blind to replay, key management and transcript design
- A 'safe' verdict is scoped to the property checked and is routinely over-read as 'correct'
- Maintenance is uneven and the headline open-source tools have seen little movement since 2024, with some vendors moving active development into hosted products — apply the same recency test you would apply to a framework before depending on one

**Choose it when:** Mandatory pre-audit hygiene for any Circom or R1CS codebase, and a permanent CI gate — so the paid engagement is not spent on findings a linter would have caught.

Maturity: Production-used, unevenly maintained · License: Mixed (MIT / GPL-3.0) · Source: https://github.com/Veridise/Picus

**In the what each assurance technique can and cannot find** (https://zkpick.com/audit/#audit-matrix-automated-underconstraint-detection)

| Technique | Layer | Characteristic finds | Blind to | Coverage claim | Cost profile |
| --- | --- | --- | --- | --- | --- |
| Automated underconstraint detection | Circuit | Non-unique outputs for a fixed input, unconstrained signals, non-strict bit decompositions | Application semantics, replay, key management, transcript design; often returns 'unknown' on hash and bigint gadgets | Per-property, where the solver terminates | Very low once wired in |

Full page: https://zkpick.com/audit/automated-underconstraint-detection/

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

Full page: https://zkpick.com/audit/formal-verification/

#### Differential and fuzz testing — *Dynamic testing*

> Differential and fuzz testing: Dynamic testing. Layer: Circuit / VM. Characteristic finds: Divergence from a reference implementation; witnesses a malicious prover could pass. Blind to: Anything the oracle also gets wrong; bug classes outside the mutation model. Coverage claim: Sampled only. Cost profile: Moderate setup, cheap to re-run. Choose it when: zkVMs, ISA and EVM emulation chips, standard cryptographic gadgets, and any circuit with an independent reference implementation. Also the right home for regression tests from prior findings.

Executing the circuit against an independent oracle and searching for divergence, or mutating the prover to simulate a malicious one and checking the constraints reject it. For zkVMs, conformance suites are the natural oracle — the RISC-V architectural certification tests and the reference tests in Ethereum's execution specs provide an externally defined notion of correct. This is how a specification-conformance bug in a formally verified zkVM was found: by conformance tests, outside the verification effort's scope.

**Strengths**

- Finds bugs manual review misses in large repetitive constraint sets
- Every finding arrives with a reproducing input, so it becomes a regression test immediately
- Runs continuously and cheaply once set up
- Metamorphic and fault-injection oracles need no full formal specification

**Tradeoffs**

- No completeness guarantee — absence of findings means nothing
- Requires a trustworthy oracle, which novel application circuits often lack
- Prover-side fuzzing needs fault injection into witness generation, which not all stacks expose
- Coverage over constraint systems is hard to define and harder to measure
- Proof generation per test case makes zkVM campaigns expensive

**Choose it when:** zkVMs, ISA and EVM emulation chips, standard cryptographic gadgets, and any circuit with an independent reference implementation. Also the right home for regression tests from prior findings.

Maturity: Research tooling with production impact · License: Mixed (GPL-3.0 / Apache-2.0) · Source: https://arxiv.org/abs/2509.10819

**In the what each assurance technique can and cannot find** (https://zkpick.com/audit/#audit-matrix-differential-and-fuzz-testing)

| Technique | Layer | Characteristic finds | Blind to | Coverage claim | Cost profile |
| --- | --- | --- | --- | --- | --- |
| Differential and fuzz testing | Circuit / VM | Divergence from a reference implementation; witnesses a malicious prover could pass | Anything the oracle also gets wrong; bug classes outside the mutation model | Sampled only | Moderate setup, cheap to re-run |

Full page: https://zkpick.com/audit/differential-and-fuzz-testing/

#### Cryptographic review of the protocol and proof system — *Cryptography review*

> Cryptographic review of the protocol and proof system: Cryptography review. Layer: Proof system. Characteristic finds: Weak Fiat–Shamir, unsound composition and recursion boundaries, wrong concrete security parameters. Blind to: Implementation defects in the circuit above it; deployment and integration issues. Coverage claim: None — argument-based. Cost profile: High; cryptographers, not circuit engineers. Choose it when: Mandatory if you implement, modify or newly compose a proof system, add recursion or aggregation, change the transcript, or pick non-standard parameters. Reducible — not eliminable — if you use a mainstream library unmodified at a pinned, audited version.

Review of the argument system itself and everything below the arithmetisation: the soundness argument and its assumptions, what the Fiat–Shamir transcript absorbs, commitment instantiation, hash and sponge parameterisation, curve and subgroup structure, recursion composition, and the concrete bit-security the chosen parameters actually imply. This layer produces the highest-impact failures because they are construction-wide rather than deployment-specific.

**Strengths**

- The only layer that can catch construction-level soundness breaks
- Findings are reusable across the ecosystem and often warrant CVEs and coordinated disclosure
- Supported by shared artefacts: the ZKProof Community Reference, ZKDocs, soundness calculators

**Tradeoffs**

- Requires cryptographers rather than circuit engineers — a different and scarcer skill set
- Hardest layer to scope and schedule; results are not predictable per reviewer-week
- Frequently skipped because the upstream library is assumed 'already audited' — which is how weak Fiat–Shamir spread across many implementations
- Concrete-security arguments for newer hash-based systems still rest on unproven assumptions

**Choose it when:** Mandatory if you implement, modify or newly compose a proof system, add recursion or aggregation, change the transcript, or pick non-standard parameters. Reducible — not eliminable — if you use a mainstream library unmodified at a pinned, audited version.

Maturity: Established discipline · License: Service · Source: https://eprint.iacr.org/2023/691

**In the what each assurance technique can and cannot find** (https://zkpick.com/audit/#audit-matrix-cryptographic-protocol-review)

| Technique | Layer | Characteristic finds | Blind to | Coverage claim | Cost profile |
| --- | --- | --- | --- | --- | --- |
| Cryptographic protocol review | Proof system | Weak Fiat–Shamir, unsound composition and recursion boundaries, wrong concrete security parameters | Implementation defects in the circuit above it; deployment and integration issues | None — argument-based | High; cryptographers, not circuit engineers |

Full page: https://zkpick.com/audit/cryptographic-review/

#### Verifier and integration review — *Human review*

> Verifier and integration review: Human review. Layer: Verifier / on-chain. Characteristic finds: Public-input aliasing and encoding mismatch, replay, verifying-key drift, missing point checks. Blind to: Circuit-internal soundness. Coverage claim: None — but the code is small. Cost profile: Low; conventional review skills. Choose it when: Every deployment. Assign one party explicit ownership of the circuit-to-verifier boundary, and require them to check the deployed verifying key against a reproducible build of the audited circuit.

Review of everything between a valid proof and a state change: the verifier contract or host routine, public input encoding and ordering, field-range validation, verifying-key provenance and immutability, nullifier storage and replay logic, upgrade authority, and the binding between the deployed key and the audited circuit. This is where circuit-correct systems still fail.

**Strengths**

- Covers a bug class that circuit tooling structurally cannot see
- Relatively cheap and fast — the code is small and conventional
- Reuses well-developed smart-contract audit practice and tooling
- Directly addresses the highest-frequency deployment failures

**Tradeoffs**

- Often split across two engagements with the seam owned by nobody — and the seam is where encoding mismatches live
- Generated verifier code is assumed correct because a tool produced it — yet generated verifiers have shipped without a field-modulus check on public signals, the input-aliasing bug
- Cannot be done meaningfully without the circuit's public-input specification

**Choose it when:** Every deployment. Assign one party explicit ownership of the circuit-to-verifier boundary, and require them to check the deployed verifying key against a reproducible build of the audited circuit.

Maturity: Production standard · License: Service · Source: https://github.com/iden3/snarkjs/issues/358

**In the what each assurance technique can and cannot find** (https://zkpick.com/audit/#audit-matrix-verifier-and-integration-review)

| Technique | Layer | Characteristic finds | Blind to | Coverage claim | Cost profile |
| --- | --- | --- | --- | --- | --- |
| Verifier and integration review | Verifier / on-chain | Public-input aliasing and encoding mismatch, replay, verifying-key drift, missing point checks | Circuit-internal soundness | None — but the code is small | Low; conventional review skills |

Full page: https://zkpick.com/audit/verifier-review/

#### Audit contests — *Crowdsourced review*

> Audit contests: Crowdsourced review. Layer: Whole scope. Characteristic finds: The long tail after targeted review; findings quick to demonstrate. Blind to: Deep cryptographic soundness work, which is under-rewarded relative to its cost. Coverage claim: None; no accountable party. Cost profile: Fixed pool, pay-for-results. Choose it when: A complement after at least one targeted review and after internal tooling is clean. Weak substitute for a cryptography review of a novel proof system.

A fixed prize pool distributed among independent researchers reviewing a pinned scope over a bounded window, weighted by severity and duplicate-adjusted. Public zkVM and circuit scopes have run in this format, with pool rules varying on whether low-severity findings are paid at all.

**Strengths**

- Wide reviewer diversity, uncorrelated with any single firm's blind spots
- Pay-for-results rather than pay-for-time
- Effective at the long tail once targeted review has covered the core
- Public scope and public results improve transparency for integrators

**Tradeoffs**

- Depth is uneven: incentives favour findings quick to demonstrate, under-rewarding deep soundness work
- The pool who can read constraint systems is far smaller than the general Solidity pool, so real coverage can be thin despite many participants
- Duplicate mechanics and severity floors distort effort allocation
- Substantial triage load on the sponsoring team
- No accountable party, no methodology statement, no coverage claim

**Choose it when:** A complement after at least one targeted review and after internal tooling is clean. Weak substitute for a cryptography review of a novel proof system.

Maturity: Production-used for ZK scopes · License: Platform · Source: https://cantina.xyz/competitions/c486d600-bed0-4fc6-aed1-de759fd29fa2

**In the what each assurance technique can and cannot find** (https://zkpick.com/audit/#audit-matrix-audit-contest)

| Technique | Layer | Characteristic finds | Blind to | Coverage claim | Cost profile |
| --- | --- | --- | --- | --- | --- |
| Audit contest | Whole scope | The long tail after targeted review; findings quick to demonstrate | Deep cryptographic soundness work, which is under-rewarded relative to its cost | None; no accountable party | Fixed pool, pay-for-results |

Full page: https://zkpick.com/audit/audit-contests/

#### Bug bounties — *Crowdsourced review*

> Bug bounties: Crowdsourced review. Layer: Deployed system. Characteristic finds: Whatever survived everything else, on the code actually running. Blind to: Everything, until someone looks — no pre-launch assurance. Coverage claim: None. Cost profile: Contingent; needs credible max payout. Maintained by: Run by the deploying team, usually on a bounty platform; the linked ZKsync Era programme is one example of a published ZK scope, not a recommendation. Choose it when: Every production system, funded proportionally to value at risk and live from mainnet day one. State explicitly whether circuits, prover, verifier contract and setup artefacts are in scope.

An open-ended funded programme covering deployed code, with published severity classification and reward scale. The better ZK programmes state explicitly whether circuits, prover, verifier contract and setup artefacts are in scope, whether completeness failures (valid inputs rejected, funds stuck) count alongside soundness failures, and what proof of concept is required at each severity.

**Strengths**

- The only mechanism covering the code you actually run, indefinitely, after every deployment
- Attracts specialists, including tool authors running new techniques against live targets
- Cost is contingent on findings rather than fixed
- Establishes a legitimate disclosure channel, reducing the chance a finder goes public instead

**Tradeoffs**

- No assurance before launch and no coverage guarantee ever
- An underfunded maximum payout is a negative signal for a system securing large value
- Scope must be drafted carefully: proof forgery for arbitrary statements must be unambiguously critical
- Demands 24/7 triage and a rehearsed emergency response

**Choose it when:** Every production system, funded proportionally to value at risk and live from mainnet day one. State explicitly whether circuits, prover, verifier contract and setup artefacts are in scope.

Maintained by: Run by the deploying team, usually on a bounty platform; the linked ZKsync Era programme is one example of a published ZK scope, not a recommendation · Maturity: Production standard · License: Platform · Source: https://immunefi.com/bug-bounty/zksyncera/

**In the what each assurance technique can and cannot find** (https://zkpick.com/audit/#audit-matrix-bug-bounty)

| Technique | Layer | Characteristic finds | Blind to | Coverage claim | Cost profile |
| --- | --- | --- | --- | --- | --- |
| Bug bounty | Deployed system | Whatever survived everything else, on the code actually running | Everything, until someone looks — no pre-launch assurance | None | Contingent; needs credible max payout |

Full page: https://zkpick.com/audit/bug-bounties/

#### LLM-assisted review — *Emerging tooling*

> LLM-assisted review: Emerging tooling. Layer: Circuit / libraries. Characteristic finds: Sustained attention over large cryptographic library surfaces (evidence so far: a single self-reported finding). Blind to: Unknown and unmeasurable; false negatives are invisible. Coverage claim: None. Cost profile: Low per run; expert triage is the real cost. Choose it when: A supplementary sweep alongside manual review and deterministic tooling, especially over large cryptographic library surfaces. Not a substitute for any other category.

Automated review pipelines built on large language models with domain-specific context engineering, run over circuit and cryptographic library code. The category has moved from speculative to evidenced: a missing subfield membership check in an optimised pairing routine was found this way, assigned a CVE, and fixed upstream. *Disclosure: that finding is the work of this document's maintainer, and it is a single self-reported result — weight it accordingly against the peer-reviewed evidence behind the other categories here.*

**Strengths**

- Sustains attention over large codebases where human reviewers fatigue
- Not restricted to a modelled bug class the way SMT and lint tooling is
- Cheap enough to re-run on every change

**Tradeoffs**

- Results depend heavily on pipeline design; naive prompting fails where context-engineered flows succeed
- No soundness or coverage guarantee; false negatives are invisible
- False positives consume expert triage time, which is the scarce resource
- Leading pipelines are proprietary and not independently reproducible, so published claims cannot be checked
- Must not be represented to third parties as equivalent to human or formal review

**Choose it when:** A supplementary sweep alongside manual review and deterministic tooling, especially over large cryptographic library surfaces. Not a substitute for any other category.

Maturity: Emerging; one CVE-assigned production finding · License: Varies; mostly proprietary · Source: https://blog.zksecurity.xyz/posts/openvm-bugs/

**In the what each assurance technique can and cannot find** (https://zkpick.com/audit/#audit-matrix-llm-assisted-review)

| Technique | Layer | Characteristic finds | Blind to | Coverage claim | Cost profile |
| --- | --- | --- | --- | --- | --- |
| LLM-assisted review | Circuit / libraries | Sustained attention over large cryptographic library surfaces (evidence so far: a single self-reported finding) | Unknown and unmeasurable; false negatives are invisible | None | Low per run; expert triage is the real cost |

Full page: https://zkpick.com/audit/llm-assisted-review/

### The engagement, start to finish

1. **Write the specification** — State the relation being proved in precise terms: inputs, outputs, what is public, what is private, what must be infeasible for an adversary. Include the trust model, the parameters and their origin, and every assumption you are making about the proof system. This document is what the audit is conducted against.
2. **Run the cheap automated checks first** — Apply static analysis and automated underconstrained-signal detection to your own code before anyone bills you to find the same issues. Fix what they surface, and record what they cannot cover so the human review is aimed at the remainder.
3. **Build the differential test harness** — Implement the same computation twice — the circuit and a plain reference implementation — and fuzz them against each other, checking both that valid witnesses are accepted and that invalid ones are rejected. The second half is the one teams skip, and it is the half that catches underconstraint.
4. **Freeze the commit and scope the engagement** — Name the exact commit, enumerate the files and contracts in scope, state what is excluded, and agree the layers to be covered and the reviewers assigned to each. Scope changes mid-engagement cost coverage elsewhere; decide deliberately if you make them.
5. **Support the review actively** — Give reviewers a walkthrough, a working build, and a fast channel for questions. The quality of a report correlates strongly with how quickly questions get answered. Do not ship changes into the audited branch while review is in progress.
6. **Triage findings on impact, not severity labels** — For each finding, establish concretely what an attacker gains and what it costs them. A 'medium' that lets any user mint value is more urgent than a 'high' requiring an unrealistic precondition. Record accepted risks explicitly, with the reasoning.
7. **Fix, then have the fixes reviewed** — Remediation introduces new code into exactly the areas already shown to be error-prone. Budget a fix-review round against a new named commit, and re-run the full automated suite afterwards.
8. **Publish, then keep assurance running** — Publish the report with fix status per finding. Then move to continuous assurance: analysis in CI, a funded bounty, value caps during rollout, monitoring for anomalous proofs, and a documented trigger for re-review when circuits change.

### The ZK bug taxonomy

- **Underconstrained signals** — The circuit admits witnesses that do not correspond to any correct execution: an intermediate value is computed in the witness but never constrained, or a constraint is weaker than the property intended. The proof verifies; it just proves less than everyone believed. This is the single most common exploitable ZK defect class.
  - *Mitigation:* Run automated underconstrained-signal detection; review that every witness-assigned value is also constrained; fuzz for accepted-but-invalid witnesses rather than only checking valid ones are accepted.
  - Full page: https://zkpick.com/audit/failure-modes/underconstrained-signals/
- **Over-constrained circuits and completeness failures** — The circuit rejects witnesses that correspond to correct executions: a range check tighter than the specification, an edge case such as zero or the field's maximum value, or a constraint that assumes an invariant the honest prover does not always satisfy. No forged proof results, so the bug is invisible to soundness tooling, but a user with a legitimate claim cannot produce a proof — funds are stuck, a withdrawal path is dead, or a rollup cannot progress until the circuit is redeployed.
  - *Mitigation:* Test completeness deliberately: generate valid witnesses across boundary values and assert the proof is produced, fuzz against a reference implementation for rejected-but-valid inputs, and include completeness in the bug-bounty scope. Tools that vet completeness as well as soundness exist for zkVMs and some circuit pipelines.
  - Full page: https://zkpick.com/audit/failure-modes/over-constrained-circuits-and-completeness-failures/
- **Missing range checks and field aliasing** — Values are assumed to fit in a bit width that is never enforced, or a value near the field modulus wraps around so that two distinct field elements represent the same logical quantity. Comparisons, sums and Merkle indices then behave in ways the developer never considered.
  - *Mitigation:* Enforce explicit range constraints on every externally influenced value, and check that decompositions into bits are both complete and canonical, rejecting non-canonical representations.
  - Full page: https://zkpick.com/audit/failure-modes/missing-range-checks-and-field-aliasing/
- **Non-deterministic or malleable witness generation** — More than one witness satisfies the constraints for the same logical input, allowing an attacker to produce a distinct valid proof for the same action — which breaks any logic that assumed proofs or their derived values are unique.
  - *Mitigation:* Constrain witness generation to a canonical form. Where uniqueness matters downstream, enforce it in the circuit rather than relying on the honest prover implementation.
  - Full page: https://zkpick.com/audit/failure-modes/non-deterministic-or-malleable-witness-generation/
- **Unsound Fiat–Shamir transcripts** — Challenges are derived from a hash that omits values it must bind — public inputs, commitments, or protocol parameters. A prover can then choose those values after seeing the challenge and forge proofs for false statements. Publicly known as the 'Frozen Heart' class, found across multiple independent implementations.
  - *Mitigation:* Hash the complete transcript, in a fixed order, including all public inputs and every commitment, with domain separation. Compare the implementation against the paper's transcript definition line by line rather than assuming the library handles it.
  - Full page: https://zkpick.com/audit/failure-modes/unsound-fiat-shamir-transcripts/
- **Public input encoding mismatch** — The circuit and the verifier disagree about how public inputs are ordered, packed, hashed or field-reduced. A proof about one statement is accepted as a proof about another, without any component behaving incorrectly in isolation.
  - *Mitigation:* Define the encoding once, in the specification, and test round-trip equivalence across every implementation of it — circuit, prover, on-chain verifier and client.
  - Full page: https://zkpick.com/audit/failure-modes/public-input-encoding-mismatch/
- **Missing nullifier or replay protection** — A valid proof can be submitted more than once, or across chains, contracts or epochs, because nothing binds it to a single use. Nullifier derivation may also be malleable, allowing distinct nullifiers for the same underlying secret.
  - *Mitigation:* Bind proofs to a domain, a chain identifier and a spending context; constrain nullifier derivation to be deterministic and collision-resistant in the circuit; check the nullifier set atomically with the state change.
  - Full page: https://zkpick.com/audit/failure-modes/missing-nullifier-or-replay-protection/
- **Unchecked curve point and subgroup membership** — Proof elements are accepted without verifying that they lie on the curve and in the correct prime-order subgroup, enabling small-subgroup and invalid-curve attacks against the verifier.
  - *Mitigation:* Validate every deserialised group element for curve membership and subgroup order before use, including in hand-written or gas-optimised verifiers where such checks are the first thing removed.
  - Full page: https://zkpick.com/audit/failure-modes/unchecked-curve-point-and-subgroup-membership/
- **Proof malleability** — A valid proof can be transformed into a different valid proof for the same statement. Any system that treats a proof hash as a unique identifier — for deduplication, nonces or replay protection — breaks.
  - *Mitigation:* Never treat proof bytes as a unique identifier. Derive uniqueness from constrained in-circuit values such as nullifiers, and canonicalise encodings on deserialisation.
  - Full page: https://zkpick.com/audit/failure-modes/proof-malleability/
- **Trusting the library's defaults** — A proof system library is used outside the assumptions its API documents: parameters reused across domains, an unsafe or testing-only setup helper left in a production path, or a security parameter left at a demo value.
  - *Mitigation:* Read the library's security notes and audit history; grep production paths for setup and testing helpers; pin and record the exact security parameters, and assert them at build time.
  - Full page: https://zkpick.com/audit/failure-modes/trusting-the-library-s-defaults/
- **Unconstrained hints not re-checked by the caller** — Modern DSLs let you compute a value outside the constraint system for efficiency — an unconstrained function, an unsafe block, a witness hint — on the understanding that the caller will constrain the result afterwards. Nothing in the language enforces that obligation, and the comment conventions surrounding it are advisory. A hint that is used but never re-constrained is an underconstrained circuit with a friendlier syntax.
  - *Mitigation:* Treat every unconstrained or unsafe block as a review checkpoint with an explicit written obligation: what the caller must verify, and where that verification happens. Grep for them and enumerate them in the audit scope rather than trusting the accompanying comment.
  - Full page: https://zkpick.com/audit/failure-modes/unconstrained-hints-not-re-checked-by-the-caller/
- **Mistaking a mock prover run for a soundness check** — A circuit development framework's mock or simulation prover confirms that the *assigned* witness satisfies the gates. It does not search for a second satisfying assignment, so it cannot detect underconstraint — yet a passing run is routinely read as evidence the circuit is correct. Related traps in the same family include missing copy constraints between regions and logic masked during key generation when values are unknown.
  - *Mitigation:* Understand exactly what your framework's test prover checks, and pair it with negative tests that mutate the witness and assert rejection, plus automated uniqueness analysis. Never treat a green mock prover run as a soundness result.
  - Full page: https://zkpick.com/audit/failure-modes/mistaking-a-mock-prover-run-for-a-soundness-check/
- **Cross-table lookup and multiplicity bugs** — In multi-table designs — zkVM chips, bus architectures — soundness depends on sends and receives balancing across tables and on multiplicity columns being correctly constrained. An unbalanced bus, an unconstrained multiplicity, or a permutation argument over the wrong tuple silently admits executions that never happened. This is a dominant recurring class in zkVM codebases and has no analogue in single-circuit review.
  - *Mitigation:* Review the bus or cross-table argument as its own artefact: enumerate every send and receive, check they balance, and confirm multiplicity columns are range-constrained and cannot be chosen freely by the prover.
  - Full page: https://zkpick.com/audit/failure-modes/cross-table-lookup-and-multiplicity-bugs/
- **Unsound recursion and aggregation boundaries** — Each layer is individually correct but their composition is not: a value committed in the inner proof is left unconstrained on an early-halt path, or the outer layer fails to check that the inner execution actually terminated. Publicly disclosed zkVM forgeries have come from exactly this pattern — two individually minor gaps at a recursion boundary combining into universal proof forgery.
  - *Mitigation:* Treat every recursion and aggregation boundary as its own review target with its own written contract: what the inner proof guarantees, what the outer layer must independently re-check, and what happens on abnormal termination. Do not assume a boundary is covered because both sides were reviewed.
  - Full page: https://zkpick.com/audit/failure-modes/unsound-recursion-and-aggregation-boundaries/
- **Soundness parameters weaker than assumed** — Configuration yields materially fewer bits of security than the team believes — commonly through FRI parameters chosen against conjectured rather than provable bounds, insufficient query counts, or grinding parameters left at defaults.
  - *Mitigation:* Write down the target soundness in bits, state whether it relies on conjectured bounds, and have the parameter derivation reviewed as an artefact in its own right — not inferred from a configuration file.
  - Full page: https://zkpick.com/audit/failure-modes/soundness-parameters-weaker-than-assumed/
- **Circuit and verifier version drift** — The deployed verifying key no longer corresponds to the audited circuit, because of a recompilation, a toolchain upgrade, or a manual key copy. Nothing detects the mismatch until proofs fail — or worse, until they succeed against the wrong relation.
  - *Mitigation:* Pin the hash of circuit artefacts and verifying keys in CI and on-chain, fail the build on mismatch, and make the deployed key hash publicly checkable against the audited commit.
  - Full page: https://zkpick.com/audit/failure-modes/circuit-and-verifier-version-drift/
- **Auditing the circuit but not the protocol** — Every constraint is correct and the system is still exploitable, because the *statement* being proved is the wrong one — front-running, griefing, economic manipulation, or a privacy leak through timing, amounts or graph structure that the proof faithfully preserves.
  - *Mitigation:* Scope protocol-level review explicitly, including privacy leakage through metadata and side channels outside the proof, and review the specification's claims about what an adversary cannot learn.
  - Full page: https://zkpick.com/audit/failure-modes/auditing-the-circuit-but-not-the-protocol/

### Sources

1. [zkSecurity — ZK security audits and cryptographic engineering](https://zksecurity.xyz/) — provider
2. [zkSecurity — public audit reports](https://zksecurity.xyz/reports/) — audit reports
3. [Clean — Lean circuit DSL developed by zkSecurity](https://github.com/Verified-zkEVM/clean) — code and documentation
4. [Introducing Clean, a formal verification DSL for ZK circuits in Lean 4 (zkSecurity)](https://blog.zksecurity.xyz/posts/clean/) — technical introduction
5. [zk.golf — circuit optimisation challenges verified in Lean 4](https://zk.golf/) — learning and practice
6. [Veridise — zero-knowledge audit services](https://veridise.com/audits/zk/) — provider
7. [Veridise — security proofs for cryptographic protocols](https://veridise.com/security/security-proofs/) — provider
8. [Zellic — ZK circuit and applied cryptography security assessments](https://www.zellic.io/) — provider
9. [0xPARC ZK Bug Tracker — bug taxonomy (frozen since late 2024; Circom/application-circuit skew)](https://github.com/0xPARC/zk-bug-tracker) — reference
10. [ZKProof Community Reference — terminology, security recommendations, standardisation](https://docs.zkproof.org/reference) — reference
11. [ZKDocs — interactive documentation on proof systems and primitives (Trail of Bits)](https://github.com/trailofbits/zkdocs) — reference
12. [Weak Fiat–Shamir Attacks on Modern Proof Systems (Dao, Miller, Wright, Grubbs)](https://eprint.iacr.org/2023/691) — paper
13. [Coordinated disclosure: Girault, Bulletproofs and PlonK (Trail of Bits)](https://blog.trailofbits.com/2022/04/13/part-1-coordinated-disclosure-of-vulnerabilities-affecting-girault-bulletproofs-and-plonk/) — disclosure
14. [The Frozen Heart vulnerability in PlonK (Trail of Bits)](https://blog.trailofbits.com/2022/04/18/the-frozen-heart-vulnerability-in-plonk/) — disclosure
15. [The Frozen Heart vulnerability in Bulletproofs (Trail of Bits)](https://blog.trailofbits.com/2022/04/15/the-frozen-heart-vulnerability-in-bulletproofs/) — disclosure
16. [Zcash counterfeiting vulnerability remediated — CVE-2019-7167, the BCTV14 setup flaw](https://electriccoin.co/blog/zcash-counterfeiting-vulnerability-successfully-remediated/) — disclosure
17. [Responsible disclosure of an SP1 zkVM exploit (LambdaClass, 3MI Labs, Aligned)](https://blog.lambdaclass.com/responsible-disclosure-of-an-exploit-in-succincts-sp1-zkvm-found-in-partnership-with-3mi-labs-and-aligned-which-arises-from-the-interaction-of-two-distinct-security-vulnerabilities/) — disclosure
18. [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) — analysis
19. [Missing subfield membership check in OpenVM pairing — CVE-2026-46669](https://blog.zksecurity.xyz/posts/openvm-bugs/) — disclosure
20. [snarkjs #358 — public signals not checked against the field modulus (input aliasing)](https://github.com/iden3/snarkjs/issues/358) — issue
21. [In-depth analysis of the zk-SNARK input aliasing vulnerability (Beosin)](https://beosin.com/resources/an-in-depth-analysis-of-zk-snark-input-aliasing-vulnerabilit) — analysis
22. [On the malleability of Groth16 proofs (Sui)](https://blog.sui.io/malleability-groth16-zkproof/) — analysis
23. [Another look at extraction and randomization of Groth's zk-SNARK](https://eprint.iacr.org/2020/811) — paper
24. [Automated detection of underconstrained circuits (QED², PLDI 2023)](https://eprint.iacr.org/2023/512) — paper
25. [Picus — automated verification of the uniqueness property for ZKP circuits (Veridise)](https://github.com/Veridise/Picus) — tool
26. [Circomspect — static analyser and linter for Circom (Trail of Bits)](https://github.com/trailofbits/circomspect) — tool
27. [It pays to be Circomspect — motivation and bug classes (Trail of Bits)](https://blog.trailofbits.com/2022/09/15/it-pays-to-be-circomspect/) — analysis
28. [CIVER — modular verification of Circom circuits, shipped as a fork of the compiler](https://github.com/costa-group/circom_civer) — tool
29. [Ecne — early automated uniqueness checking for R1CS](https://github.com/franklynwang/EcneProject) — tool
30. [Coda — refinement types for verifying Circom circuits in Coq](https://github.com/Veridise/Coda) — tool
31. [Practical security analysis of ZKP circuits (ZKAP, USENIX Security '24)](https://www.usenix.org/conference/usenixsecurity24/presentation/wen) — paper
32. [halo2-analyzer / Korrekt — abstract interpretation and SMT analysis of PLONKish circuits](https://github.com/quantstamp/halo2-analyzer) — tool
33. [Automated analysis of Halo2 circuits](https://eprint.iacr.org/2023/1051) — paper
34. [CCC-Check — language-agnostic detection of computation-constraint inconsistencies in ZKP programs via value inference](https://eprint.iacr.org/2025/2120) — paper
35. [zkFuzz — fuzzing framework for zero-knowledge circuits](https://arxiv.org/abs/2504.11961) — paper
36. [Circuzz — fuzzing ZK processing pipelines (ACM CCS 2025)](https://mariachris.github.io/Pubs/CCS-2025.pdf) — paper
37. [Arguzz — testing zkVMs for soundness and completeness bugs (USENIX Security '26)](https://arxiv.org/abs/2509.10819) — paper
38. [Automated soundness and completeness vetting of Polygon zkEVM (USENIX Security '25)](https://www.usenix.org/conference/usenixsecurity25/presentation/peng-xinghao) — paper
39. [Verified zk(E)VM project — Ethereum Foundation formal verification effort](https://verified-zkevm.org/) — project
40. [clean — Lean 4 DSL for writing and formally verifying ZK circuits](https://github.com/Verified-zkEVM/clean) — tool
41. [ArkLib — formally verified arguments of knowledge in Lean](https://github.com/Verified-zkEVM/ArkLib) — tool
42. [Formal verification of Halo2 circuits in Lean (Halva, Nethermind)](https://www.nethermind.io/blog/formal-verification-of-halo2-circuits-in-lean) — analysis
43. [Comparison of formal verification frameworks for arithmetic circuits](https://blog.zksecurity.xyz/posts/formal-verification-arithmetic-circuits/) — analysis
44. [soundcalc — soundness calculator across hash-based zkEVMs (Ethereum Foundation)](https://github.com/ethereum/soundcalc) — tool
45. [zkEVM security overview — multiproof redundancy, testing, audits, formal verification](https://zkevm.ethereum.foundation/blog/zkevm-security-overview) — reference
46. [ZK audit checklist — concrete per-category audit checks](https://github.com/PositiveSecurity/zk-audit-guide) — reference
47. [RISC-V architectural certification tests — conformance oracle for RISC-V zkVMs](https://github.com/riscv/riscv-arch-test) — test suite
48. [Ethereum execution specs — reference tests for zkEVM conformance (absorbed the former execution-spec-tests)](https://github.com/ethereum/execution-specs) — test suite