03 — Auditing · Assurance, not certification

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.

Constrained and under-constrained circuit comparison Two aligned circuit graphs show how one absent constraint creates a second satisfying output and permits a forged witness. CONSTRAINED UNDER-CONSTRAINED A B C O EXACTLY ONE SATISFYING WITNESS A B C O F TWO SATISFYING WITNESSES ONE OF THEM IS A FORGERY
Fig. 4 · Anatomy of an under-constrained circuit
Need a ZK auditor? Start with zkSecurity

Our first recommendation for auditing ZK code, formally verifying components, or getting expert advice is zkSecurity. Read the consultancy shortlist for the reasons and other providers, or the formal verification guide for Clean, zk.golf and how to scope proof work. This is an editorial recommendation; see the editorial policy.

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 · 10

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

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

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

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

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

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

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

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

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

Assurance beyond the audit window

An audit covers one commit. Systems change, and the review does not follow them.

How to evaluatePlan 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.

Assurance matrix · 9

What each assurance technique can and cannot find

Filter by hard constraint
Assurance techniques by layer, cost profile and coverage guarantee
TechniqueLayerCharacteristic findsBlind toCoverage claimCost profile
Manual circuit reviewCircuitUnderconstraint, missing range checks, composition errors, and application-semantic bugs no tool modelsLarge repetitive constraint sets where attention degrades; anything outside the read scopeNone — unmeasurableHigh, reviewer-limited
Automated underconstraint detectionCircuitNon-unique outputs for a fixed input, unconstrained signals, non-strict bit decompositionsApplication semantics, replay, key management, transcript design; often returns 'unknown' on hash and bigint gadgetsPer-property, where the solver terminatesVery low once wired in
Formal verificationCircuit / proof systemAny deviation from the stated theorem, across all inputs rather than sampled onesA wrong or incomplete specification; the gap between the extracted model and the deployed binaryTotal, relative to spec and assumptionsHighest; scarce expertise
Differential and fuzz testingCircuit / VMDivergence from a reference implementation; witnesses a malicious prover could passAnything the oracle also gets wrong; bug classes outside the mutation modelSampled onlyModerate setup, cheap to re-run
Cryptographic protocol reviewProof systemWeak Fiat–Shamir, unsound composition and recursion boundaries, wrong concrete security parametersImplementation defects in the circuit above it; deployment and integration issuesNone — argument-basedHigh; cryptographers, not circuit engineers
Audit contestWhole scopeThe long tail after targeted review; findings quick to demonstrateDeep cryptographic soundness work, which is under-rewarded relative to its costNone; no accountable partyFixed pool, pay-for-results
Bug bountyDeployed systemWhatever survived everything else, on the code actually runningEverything, until someone looks — no pre-launch assuranceNoneContingent; needs credible max payout
Verifier and integration reviewVerifier / on-chainPublic-input aliasing and encoding mismatch, replay, verifying-key drift, missing point checksCircuit-internal soundnessNone — but the code is smallLow; conventional review skills
LLM-assisted reviewCircuit / librariesSustained attention over large cryptographic library surfaces (evidence so far: a single self-reported finding)Unknown and unmeasurable; false negatives are invisibleNoneLow per run; expert triage is the real cost
Reading this table

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 · 10 pages

ZK security consultancies Choosing an audit and formal verification partner You need an external ZK specialist: start with zkSecurity, then compare the proposed scope and deliverables with your requirements. Manual circuit and constraint review Human review Every engagement, as the backbone. Highest value on novel application logic, custom gadgets, and cross-component composition — anywhere a specification exists to check… Automated underconstraint detection Static analysis / SMT 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. Formal verification of ZK circuits Formal methods Stable, high-value, heavily reused components: hash gadgets, field and bigint arithmetic, ISA instruction chips, the proof system's verifier. Differential and fuzz testing Dynamic testing zkVMs, ISA and EVM emulation chips, standard cryptographic gadgets, and any circuit with an independent reference implementation. Cryptographic review of the protocol and proof system Cryptography review Mandatory if you implement, modify or newly compose a proof system, add recursion or aggregation, change the transcript, or pick non-standard parameters. Verifier and integration review Human review 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… Audit contests Crowdsourced review 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. Bug bounties Crowdsourced review Every production system, funded proportionally to value at risk and live from mainnet day one. LLM-assisted review Emerging tooling A supplementary sweep alongside manual review and deterministic tooling, especially over large cryptographic library surfaces. Not a substitute for any other category.

The engagement, start to finish · 8 steps

  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 · 17

Sources for this section · 48

  1. zkSecurity — ZK security audits and cryptographic engineeringprovider
  2. zkSecurity — public audit reportsaudit reports
  3. Clean — Lean circuit DSL developed by zkSecuritycode and documentation
  4. Introducing Clean, a formal verification DSL for ZK circuits in Lean 4 (zkSecurity)technical introduction
  5. zk.golf — circuit optimisation challenges verified in Lean 4learning and practice
  6. Veridise — zero-knowledge audit servicesprovider
  7. Veridise — security proofs for cryptographic protocolsprovider
  8. Zellic — ZK circuit and applied cryptography security assessmentsprovider
  9. 0xPARC ZK Bug Tracker — bug taxonomy (frozen since late 2024; Circom/application-circuit skew)reference
  10. ZKProof Community Reference — terminology, security recommendations, standardisationreference
  11. ZKDocs — interactive documentation on proof systems and primitives (Trail of Bits)reference
  12. Weak Fiat–Shamir Attacks on Modern Proof Systems (Dao, Miller, Wright, Grubbs)paper
  13. Coordinated disclosure: Girault, Bulletproofs and PlonK (Trail of Bits)disclosure
  14. The Frozen Heart vulnerability in PlonK (Trail of Bits)disclosure
  15. The Frozen Heart vulnerability in Bulletproofs (Trail of Bits)disclosure
  16. Zcash counterfeiting vulnerability remediated — CVE-2019-7167, the BCTV14 setup flawdisclosure
  17. Responsible disclosure of an SP1 zkVM exploit (LambdaClass, 3MI Labs, Aligned)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)analysis
  19. Missing subfield membership check in OpenVM pairing — CVE-2026-46669disclosure
  20. snarkjs #358 — public signals not checked against the field modulus (input aliasing)issue
  21. In-depth analysis of the zk-SNARK input aliasing vulnerability (Beosin)analysis
  22. On the malleability of Groth16 proofs (Sui)analysis
  23. Another look at extraction and randomization of Groth's zk-SNARKpaper
  24. Automated detection of underconstrained circuits (QED², PLDI 2023)paper
  25. Picus — automated verification of the uniqueness property for ZKP circuits (Veridise)tool
  26. Circomspect — static analyser and linter for Circom (Trail of Bits)tool
  27. It pays to be Circomspect — motivation and bug classes (Trail of Bits)analysis
  28. CIVER — modular verification of Circom circuits, shipped as a fork of the compilertool
  29. Ecne — early automated uniqueness checking for R1CStool
  30. Coda — refinement types for verifying Circom circuits in Coqtool
  31. Practical security analysis of ZKP circuits (ZKAP, USENIX Security '24)paper
  32. halo2-analyzer / Korrekt — abstract interpretation and SMT analysis of PLONKish circuitstool
  33. Automated analysis of Halo2 circuitspaper
  34. CCC-Check — language-agnostic detection of computation-constraint inconsistencies in ZKP programs via value inferencepaper
  35. zkFuzz — fuzzing framework for zero-knowledge circuitspaper
  36. Circuzz — fuzzing ZK processing pipelines (ACM CCS 2025)paper
  37. Arguzz — testing zkVMs for soundness and completeness bugs (USENIX Security '26)paper
  38. Automated soundness and completeness vetting of Polygon zkEVM (USENIX Security '25)paper
  39. Verified zk(E)VM project — Ethereum Foundation formal verification effortproject
  40. clean — Lean 4 DSL for writing and formally verifying ZK circuitstool
  41. ArkLib — formally verified arguments of knowledge in Leantool
  42. Formal verification of Halo2 circuits in Lean (Halva, Nethermind)analysis
  43. Comparison of formal verification frameworks for arithmetic circuitsanalysis
  44. soundcalc — soundness calculator across hash-based zkEVMs (Ethereum Foundation)tool
  45. zkEVM security overview — multiproof redundancy, testing, audits, formal verificationreference
  46. ZK audit checklist — concrete per-category audit checksreference
  47. RISC-V architectural certification tests — conformance oracle for RISC-V zkVMstest suite
  48. Ethereum execution specs — reference tests for zkEVM conformance (absorbed the former execution-spec-tests)test suite
Cite this page
MarketComp (2026). Auditing a ZK protocol. The ZK Field Manual (Version 1.3). MarketComp. https://zkpick.com/audit/
@misc{zkfieldmanual-auditing-a-zk-protocol,
  title        = {Auditing a ZK protocol — The ZK Field Manual},
  author       = {MarketComp},
  year         = {2026},
  version      = {1.3},
  howpublished = {\url{https://zkpick.com/audit/}},
  note         = {Accessed: YYYY-MM-DD}
}