Bonus — ZK Circuit Security for Web3 Auditors

“Most Web3 auditors will never write a Circom template, will never prove a polynomial identity on paper, and will never run a Groth16 ceremony. But every auditor will, at some point, sit across the table from a team that says ‘and there is a ZK proof here’ — and at that moment, the auditor has to decide whether to nod, defer, or push back. This lesson teaches you what to push back on, what to defer on, and the one bug class that is responsible for the overwhelming majority of real-world ZK exploits. You do not leave this lesson a circuit engineer. You leave with the language, the smell test, and the courage to say ‘I want a separate cryptographer-led audit of this circuit before I sign off on the system that depends on it.‘”

Tags: web3-security zk zero-knowledge circuits soundness under-constrained circom halo2 noir bonus Learner: Past Tuan-01-Web3-Blockchain-Crypto-Fundamentals (you remember the ZK paragraph in §4.6) and ideally Tuan-11-L2-Rollup-Modular-Security (you know what a validity proof gates on the L1 bridge). Strong programming background, comfort with abstract algebra is a bonus but not required. Time: 5–7 days (4–5h/day). This is a bonus chapter; treat it as an investment in vocabulary and risk triage, not as a path to becoming a circuit auditor. Related: Tuan-01-Web3-Blockchain-Crypto-Fundamentals · Tuan-11-L2-Rollup-Modular-Security · Tuan-10-Bridge-Cross-Chain-Security · Tuan-Bonus-Formal-Verification-Deep · Tuan-15-Audit-Methodology-Tooling

1. Context & Why

1.1 The honest framing

Let’s start with a confession that most ZK course material avoids: the median Web3 auditor in 2026 does not audit circuits. Circuit auditing is a specialization. The people who do it well are a small population, mostly concentrated at Veridise, zkSecurity, Trail of Bits, Zellic, ABDK, Spearbit (a few engagers), PSE Audits, and a handful of independents. They have backgrounds in algebraic geometry, computer algebra, or formal verification. Their day rate reflects the supply curve.

So why teach you anything? Because the surface that depends on a ZK circuit is enormous and growing:

ZK rollups publish state roots and validity proofs that gate billions of dollars of L1 bridge withdrawals. You audited the bridge and the rollup architecture — but the bridge unlocks funds when a verifier contract returns true. The verifier contract checks a proof. The proof attests to a circuit. The circuit was written by humans. If the circuit is under-constrained, the proof verifies “correctly” against an invalid state transition, and the bridge pays out.
ZK identity / privacy (Semaphore, Worldcoin’s World ID, Sismo, zkPass, zkEmail, Anon Aadhaar). A circuit attests “I am a unique human” or “this email is from this domain”. An under-constrained circuit lets one person mint many proofs, or lets anyone forge an attestation.
ZK coprocessors / oracles (Axiom, Herodotus, Lagrange) prove statements about historical chain state. Wrong proof → wrong on-chain action.
Privacy mixers / shielded pools (Tornado Cash historically, Aztec, Nocturne, Railgun). The circuit enforces “I’m withdrawing what I deposited and not double-spending”. Soundness break → infinite mint.
General application circuits that protocols increasingly write themselves (zk-NFTs, private votes, KYC-light schemes, fraud-proof inner circuits for hybrid systems).

Your job in this lesson is not to become the person who finds the under-constrained constraint. Your job is to:

Speak the language well enough to read a ZK section of an architecture spec without bluffing.
Map the threat surface so when you scope an audit you can identify “this part needs a cryptographer; this part is normal Solidity work”.
Recognize the dominant bug class — under-constrained circuits — by shape, even if you can’t always fix it.
Audit the integration points that surround the circuit: the on-chain verifier contract, the public-input handling, the trusted-setup ceremony hygiene, the prover infrastructure, the post-verification semantics. These integration points are normal Web3 auditor work and they are where many “ZK bugs” actually live.

Whoever tells you ZK is just “trust the math” is selling you something. The math is the cheap part. The expensive part is the engineering between the math and the user, and that’s where your auditor reflexes apply.

1.2 The auditor’s reframe of “zero-knowledge proof”

Strip the cryptography. A ZK proof system gives a program two interfaces:

Prover(public_input, private_witness) → proof
Verifier(public_input, proof)         → bool

The system promises three properties:

Property	What it means	What breaks if violated
Completeness	Honest prover with valid `(public_input, witness)` always produces a proof that verifies	Honest user can’t use the system. Rare bug, usually caught in testing
Soundness	A prover without a valid witness satisfying the predicate cannot make the verifier accept (except with negligible probability)	A malicious prover convinces the verifier of a false statement. This is where money is lost
Zero-knowledge	The proof reveals nothing about the witness beyond what the public input implies	Privacy leak. Usually about randomness in proving

For a Web3 auditor, soundness is the property to fixate on. Completeness failures are correctness bugs that the dev team will notice during integration testing. Zero-knowledge failures are privacy bugs and matter for shielded-pool / identity protocols specifically. Soundness failures are wealth-destroying because they let an attacker prove false statements that bridge contracts and verifier contracts then act on.

The dominant soundness failure mode is under-constrained circuits, and that’s the bug class we’ll spend the most time on.

1.3 What you’ll be able to do at the end

Define soundness, completeness, and zero-knowledge in one paragraph each, including a concrete consequence of each failure.
Read a 50-line Circom file and ask the right four questions: which signals are public, which are private, which constraints are present, which constraints are not present.
Articulate the difference between Groth16 (trusted setup, per-circuit), PLONK / KZG (universal trusted setup), and STARK (transparent, post-quantum), and state which trade-off matters when.
Identify five sub-patterns of under-constrained circuit bugs (missing range check, missing bit decomposition, missing zero check, signed/unsigned confusion, nondeterminism) by shape.
Read an on-chain Solidity Verifier and explain what each input[i] represents in the upstream circuit — and flag the bug class where the on-chain caller passes garbage in input[i].
Run circomspect on a sample circuit and interpret the warnings.
Triage a “this protocol uses ZK” claim: decide whether your audit scope should include the circuit, recommend specialist engagement, or carve it out explicitly.

1.4 Primary references

Source	URL	Why
Circom docs	https://docs.circom.io/	The most accessible circuit DSL; reference syntax for this lesson
circomlib	https://github.com/iden3/circomlib	Standard Circom library; many real-world bugs sit in mis-use of these templates
Halo2 (Zcash) book	https://zcash.github.io/halo2/	The Halo2 PLONKish proof system; used by Zcash, PSE zkEVM, some custom circuits
Noir (Aztec) docs	https://noir-lang.org/docs/	High-level Rust-like circuit language; cleaner abstractions, but the same underlying bug classes apply
Cairo (Starknet)	https://book.cairo-lang.org/	Production Cairo; used by Starknet’s STARK-based execution
Plonky2 / Plonky3	https://github.com/0xPolygonZero/plonky2 · https://github.com/Plonky3/Plonky3	Polygon’s recursion-friendly proof system; underpins many ZK-EVMs in 2025–2026
0xPARC ZK Bug Tracker	https://github.com/0xPARC/zk-bug-tracker	The canonical catalog of real-world ZK bugs; required reading
Trail of Bits — zkdocs	https://github.com/trailofbits/publications · https://github.com/trailofbits/zkdocs	ToB’s pragmatic ZK security writeups; includes circomspect documentation
Veridise — Picus and ZK audit blog	https://veridise.com/ · https://github.com/Veridise/Picus	Picus = under-constrained detector; Veridise blog has dozens of real bug writeups
Zellic ZK research	https://www.zellic.io/blog/	Search for `zk`, `circom`, `halo2`; rigorous post-mortems
Privacy & Scaling Explorations (PSE)	https://pse.dev/	Ethereum Foundation’s applied-ZK research org; many open-source circuits and audits
ZK Hack puzzles + writeups	https://zkhack.dev/	CTF-style ZK challenges; the writeups are the cheapest crash course in soundness intuition
”Why and How zk-SNARK Works” (Petkus)	https://arxiv.org/abs/1906.07221	The clearest “how SNARKs work under the hood” tutorial for engineers
Vitalik — “Quadratic Arithmetic Programs”	https://medium.com/@VitalikButerin/quadratic-arithmetic-programs-from-zero-to-hero-e6d558cea649	Foundational intuition; old but still pedagogically right
L2Beat — Stage validity-proof status per chain	https://l2beat.com/scaling/risk	Live state of which ZK rollups have battle-tested provers

Currency note: ZK tooling moves fast. Specific tool versions, prover backends, and ceremony states change quarterly. Treat all version-specific claims in this lesson as [verify] at audit time. The bug taxonomy is durable; the tooling snapshot is not.

2. ZK Basics, Audit Depth

2.1 What “proof” means here

In normal Web3 speech, “proof” can mean a Merkle proof, an ECDSA signature, a sworn affidavit, or a ZK proof. They are different. For this chapter, a proof is a short string π produced by a prover that lets a verifier check, in time much less than the cost of re-executing the original computation, that some predicate holds on a public input.

The predicate has the form:

∃ witness w. f(public_input, w) = true

The verifier learns “such a w exists” without learning w. The proof is succinct (small enough to put on-chain, typically a few hundred bytes to a few KB). Verification is fast (single milliseconds; on-chain in 200k–600k gas for typical SNARKs, more for STARKs).

The prover does the hard work: turns the predicate into an arithmetic circuit, finds a witness, runs polynomial machinery, outputs π. The prover’s machine cost can be enormous (minutes to hours per proof for complex circuits; this is why zk-EVMs are economically tight).

2.2 SNARK vs STARK — the choice that propagates

A SNARK (“Succinct Non-interactive ARgument of Knowledge”) and a STARK (“Scalable Transparent ARgument of Knowledge”) are two families of proof system. Both produce short proofs. They differ in:

Property	SNARK (Groth16, PLONK, Halo2)	STARK (Starknet, Plonky2 STARK mode, Polygon Miden)
Trusted setup	Groth16: per-circuit. PLONK / KZG: universal one-time. Halo2 IPA: none (transparent SNARK)	None (“transparent”)
Proof size	~200 B (Groth16) to ~1 KB (PLONK)	~50–200 KB (much larger)
Verifier gas (on-chain)	~200k–400k for Groth16; ~400k–600k for KZG-PLONK	~5M+ on Ethereum L1 (impractical without recursion or alternative L1)
Cryptographic assumption	Pairing-based + DLP (not post-quantum)	Collision-resistant hashing only (post-quantum safe)
Recursion friendliness	Halo2, Nova, accumulation schemes are designed for it	Native to STARK (FRI commitment scheme recurses naturally)
Prover cost	High (pairings, FFTs)	Higher per step but parallelism-friendly

Audit-relevant takeaways:

Groth16’s per-circuit trusted setup is a trust assumption that doesn’t go away. Even after a “good” ceremony, the toxic waste — the random values used during setup — must have been deleted by at least one participant. If all participants colluded, they retain the ability to forge proofs for that exact circuit. Audit angle: who ran the ceremony, how many participants, is the transcript published, can you re-verify the contribution chain?
PLONK / KZG universal setup means one ceremony serves all circuits up to a max size. Less per-deployment risk, but still a one-time toxic-waste concern.
STARK / FRI transparent has no toxic waste, but proofs are bigger and on-chain verification is more expensive — usually mitigated by wrapping a STARK proof inside a SNARK for final on-chain submission (“STARK→SNARK wrap” pattern; Polygon zkEVM and several other systems do this).
Post-quantum: SNARKs based on elliptic-curve pairings break in the presence of a sufficient quantum computer. STARKs don’t. In 2026 this is a theoretical concern but the L2s that care are choosing accordingly.

When you read a protocol spec that says “we use Groth16 over BN254”, you should immediately note: per-circuit trusted setup, ~200 byte proofs, ~200k gas verifier, not post-quantum, pairing-based. When it says “we use Halo2 with IPA”, you note: no trusted setup, recursion-friendly, larger verifier cost on-chain. Each choice has audit consequences.

2.3 The proving stack — what each layer is

flowchart TB
  subgraph App[Application Layer]
    Spec["Spec: 'prove I withdrew only what I deposited'"]
  end
  subgraph DSL[Circuit DSL]
    Circom[Circom / Noir / Cairo / Halo2]
  end
  subgraph IR[Intermediate Representation]
    R1CS[R1CS / PLONKish / AIR]
  end
  subgraph Proof[Proof System]
    PS[Groth16 / PLONK / Halo2 / STARK]
  end
  subgraph Verifier[On-chain Verifier]
    Sol[Solidity Verifier.sol]
  end
  subgraph App2[On-chain consumer]
    Bridge[Bridge / Pool / Identity contract]
  end

  Spec --> Circom --> R1CS --> PS --> Sol --> Bridge
  style Spec fill:#fff2cc
  style Circom fill:#dde
  style R1CS fill:#ddd
  style PS fill:#dde
  style Sol fill:#fcd
  style Bridge fill:#fcd

Where bugs live, by layer:

Layer	Typical bug	Who finds it
App spec	Spec doesn’t match the actual security property the protocol wants	Protocol designer / lead auditor
Circuit DSL	Under-constrained circuit — most ZK bugs are here	Circuit-specialist auditor (Veridise / ToB / Zellic / specialist independents)
IR / proof system	Cryptographic bug in proof system implementation; rare but catastrophic	Cryptographer / academic research
On-chain verifier	Wrong public input layout, wrong domain, replay-able proofs, upgradeable verifier with weak admin	General Web3 auditor (you)
On-chain consumer	The contract that calls `verifier.verifyProof(...)` — does it correctly bind the public input to its action?	General Web3 auditor (you)

This is the practical division of labor. You are not (yet) auditing the circuit. You are auditing what surrounds it. But you should be able to read it well enough to (a) tell a circuit specialist what specifically to look at, and (b) catch the obvious “the public input includes recipient but on-chain we use a different recipient” mismatches that, by the way, have caused real losses.

2.4 Recursive proofs — what they buy and what to worry about

Recursive proof composition: a proof can prove the validity of another proof.

π_inner attests to f(x, w) = true
π_outer attests to "I verified π_inner correctly, and π_inner attests to predicate P"

Three places recursion shows up in production:

Proof aggregation — many small proofs aggregated into one to amortize on-chain verifier cost (e.g., a zk-rollup batches many transaction proofs into one block proof).
STARK→SNARK wrap — generate a fast-prover STARK and then a smaller-verifier SNARK over it. Used by Polygon, occasionally others.
Incrementally Verifiable Computation (IVC) — Nova, SuperNova, ProtoStar accumulation schemes. The frontier; powers some 2025–2026 chain-wide proving stacks.

Audit angles on recursion:

Security composition: if the inner proof has soundness error 2^-80 and the outer wraps it once, your effective soundness depends on the composition theorem of the proof system. Most are fine; some pathological constructions stack errors. Defer to a cryptographer if the protocol claims “novel recursion scheme”.
Public-input binding: when proof A is wrapped by proof B, B must verify A’s exact public input. A protocol that lets B verify A without binding the input list is wide open — attacker generates a valid A on input x' and a B that “verified A” without specifying x'. Always trace public-input flow through wrappers.
Verifier-of-verifier complexity: the on-chain verifier may itself be a recursive verifier. The Solidity code becomes harder to read; bugs hide in the bigger surface.

3. Circuit DSLs — the lay of the land

You’ll encounter five major DSLs in 2026. Each makes different trade-offs.

3.1 Circom (iden3)

pragma circom 2.1.6;

template IsZero() {
    signal input in;
    signal output out;
    signal inv;

    inv <-- in != 0 ? 1/in : 0;
    out <== -in * inv + 1;
    in * out === 0;
}

Properties:

Arithmetic-circuit DSL: each line either declares a signal or imposes a constraint.
The <== operator both assigns and constrains. The <-- operator assigns without constraining (escape hatch; this is where most bugs live).
The === operator imposes a constraint without assignment.
Compiles to R1CS (Rank-1 Constraint System), which Groth16 and PLONK consume.
Standard library: circomlib (Num2Bits, LessThan, MultiMux1, etc.). Many real-world bugs come from misusing these templates.

Why it dominates ZK security writeups: Circom is the most-deployed DSL for application circuits (Tornado Cash, Semaphore, World ID’s earlier circuits, many small protocols). Most public bug post-mortems are Circom. If you only learn one DSL for audit reading, learn Circom.

3.2 Halo2 (Zcash / PSE)

Halo2 is a Rust framework for writing PLONKish circuits — generalized PLONK with custom gates and lookup arguments. Zcash uses it (Orchard); PSE uses it for the zkEVM; many newer ZK rollups choose it.

// Sketch of a Halo2 gate (illustrative)
meta.create_gate("is_zero", |meta| {
    let in_ = meta.query_advice(in_col, Rotation::cur());
    let out = meta.query_advice(out_col, Rotation::cur());
    let inv = meta.query_advice(inv_col, Rotation::cur());
    let s = meta.query_selector(s_is_zero);
    vec![
        s.clone() * (out.clone() - (Expression::Constant(F::ONE) - in_.clone() * inv)),
        s * in_ * out,
    ]
});

Audit reality: Halo2 circuits are harder for general auditors to read than Circom. The “gate” abstraction means you’re reading polynomial expressions over column queries. You will not audit a Halo2 circuit as a generalist. You will see that a protocol uses Halo2 and you will recommend a specialist. But you should be able to look at a Halo2 spec and know what to ask for.

3.3 Noir (Aztec)

Noir aims to make circuit programming feel like Rust:

// Sketch
fn main(x: Field, y: pub Field) {
    let z = x * x;
    assert(z == y);
}

pub marks public inputs; everything else is witness. The compiler handles constraint generation. Pedagogically the cleanest DSL in 2026 and the one that minimizes “easy to under-constrain” footguns by hiding the unconstrained-assignment escape hatch (<-- style) behind explicit unsafe patterns.

Caveat: Noir is younger, the standard library is less battle-tested, and the “easier to read” interface can hide bugs at the assertion level (you can still write a circuit that doesn’t actually constrain what you think it does — the assertion is on a value, but is the value derived from the right inputs?).

3.4 Cairo (Starknet)

Cairo is Starknet’s VM-targeted language. Not a circuit DSL in the Circom sense — Cairo programs run on the Cairo VM, and the VM’s execution is the thing that gets STARK-proven. From the auditor’s view:

The “circuit” is implicit (it’s the Cairo VM trace). The auditor reads Cairo code as a normal program, with the awareness that it’s being proven for execution correctness.
Soundness bugs at the Cairo program level look like normal program bugs (logic errors).
Soundness bugs at the VM constraint level are the Starkware team’s problem and have had public incidents historically ([verify] — Starknet has had prover constraint bugs).

For audit purposes, treat Cairo as “a smart-contract language with weird types (felt252) and a different VM” and let the StarkWare core team’s audits cover the VM proving layer.

3.5 Plonky2 / Plonky3 (Polygon Zero)

Plonky2 (2022) and Plonky3 (2024) are Polygon Zero’s high-performance proof systems. Used by Polygon zkEVM (in part), Polygon Miden, and increasingly by independent rollup projects.

You generally don’t write circuits directly in Plonky2 the way you do in Circom; you use higher-level languages that compile to it, or you write Rust against the plonky2 crate. Audit posture: same as Halo2 — defer to specialists, but be able to recognize the stack.

3.6 Choosing what to focus on

For a generalist auditor in 2026, the prioritization:

Circom — read fluently. Most public bug examples are here. The ZK Bug Tracker examples are mostly Circom. If you can read Circom comfortably, you can interpret most ZK postmortems.
Noir — recognize and read at intermediate level. Aztec’s adoption is real and growing; many newer protocols default to Noir.
Halo2 / Plonky2 / Cairo — recognize and triage. You don’t read them line-by-line, but you know what they are, what trade-offs they make, and you can articulate “this needs a specialist with Halo2 experience” when scoping.

4. The Dominant Bug Class — Under-constrained Circuits

This section is the meat of the lesson.

4.1 The core insight

A circuit is a system of arithmetic constraints over a finite field. A witness is an assignment of values to all signals such that every constraint is satisfied. A valid witness is one that, in addition to satisfying constraints, corresponds to the application’s intended semantics.

The proof system guarantees: the proof verifies if and only if the prover knows a witness that satisfies the constraints. The proof system does not know anything about your application’s intended semantics. If your constraints are weaker than your semantics, the proof system will happily verify witnesses that satisfy constraints but violate intent.

Under-constrained circuit = the circuit’s constraints permit witnesses that the developer didn’t intend.

Application's intended set of valid (input, witness) pairs  ⊊  Set of witnesses satisfying circuit constraints
                                                            ↑
                                                            attacker space

Every under-constrained bug is a member of the right-hand minus left-hand difference set. The attacker picks any element there, generates a proof, and the verifier accepts.

This is the soundness bug pattern. It is the dominant pattern. The 0xPARC ZK Bug Tracker lists dozens of real instances; the overwhelming majority are some shape of under-constrained constraint.

4.2 The canonical “IsZero” template — and what’s special about it

Look at this Circom template, which is in circomlib and used everywhere:

template IsZero() {
    signal input in;
    signal output out;
    signal inv;

    inv <-- in != 0 ? 1/in : 0;
    out <== -in * inv + 1;
    in * out === 0;
}

Let’s read it as an auditor.

Spec: out == 1 iff in == 0; out == 0 otherwise.

Constraints actually enforced:

out == -in * inv + 1 ⟺ out + in*inv == 1 (from <==)
in * out == 0 (from ===)

(Note: inv <-- ... uses <--, which is an assignment hint to the prover and imposes no constraint.)

Let’s check: are these two constraints enough?

If in == 0: constraint 1 gives out + 0 == 1, so out = 1. Constraint 2 gives 0 * 1 == 0, satisfied. So (in=0, out=1) is the only witness. ✓
If in != 0: constraint 2 says in * out == 0. Since in != 0 in a field with no zero divisors, out == 0. Substituting into constraint 1: 0 = -in*inv + 1, so inv = 1/in. So (in≠0, out=0, inv=1/in) is the only witness. ✓

So the two-constraint formulation is sound. The inv <-- line is not a soundness contributor — it’s a completeness helper. The prover needs to know how to compute inv. The constraints alone tell the verifier that if the prover supplied an inv, the (in, out) pair must be the intended one.

The audit moves to make on every Circom template:

Identify every <--. These are unconstrained assignments. They must be redundant (the values are also pinned down by ===/<== constraints elsewhere) or the circuit is under-constrained.
Identify every === and <==. These are constraints. List them as polynomial equations.
Quantify what the constraints permit. For each declared input, ask: “what is the full set of witness assignments that satisfy these constraints?” If that set is strictly larger than the application’s intended set, you have an under-constraint.

For complex circuits, this is what tools like Picus, Coda, circomspect, and Ecne automate. But the intuition stays the same: constraints are what hold; assignments are what hint.

4.3 Sub-pattern 1: missing range check

The most common under-constraint bug. The circuit assumes a signal is in a range (e.g., 0 ≤ x < 2^32) but doesn’t enforce it.

// Vulnerable: x is supposed to be a uint32 representing a coin amount
template TransferCheck() {
    signal input x;        // amount
    signal input balance;
    signal output ok;

    // Intended: ok == 1 if x <= balance
    // Naive comparison via subtraction:
    signal diff;
    diff <== balance - x;
    // diff should be "non-negative" — but in F_p there is no "non-negative"
    // The developer forgets that F_p elements are 0..p-1; "balance < x" wraps around.

    component isz = IsZero();
    isz.in <== diff;
    ok <== 1 - isz.out;  // if diff != 0, ok = 1 (the wrong check, but let's keep going)
}

The bug: F_p arithmetic has no “negative” numbers. If x > balance, balance - x doesn’t go negative — it wraps to p - (x - balance), a huge positive field element. The circuit accepts this as valid because the developer never enforced that x fits in a small range.

Fix: explicitly decompose x and balance into bits and check the high bit of (balance - x) after fitting in n+1 bits. circomlib’s LessThan(n) template does this — but only if you actually use it, and only if you pass the right n for the actual bit-width.

Real-world shape: this is the “signed/unsigned confusion” class. zk-rollup circuits, ZK identity attribute proofs (“age > 18”), and ZK voting amount checks have all had variants of this bug. The 0xPARC ZK Bug Tracker has multiple entries fitting this pattern.

4.4 Sub-pattern 2: missing bit-decomposition constraints

The Num2Bits(n) template in circomlib is supposed to:

Decompose a number into n bits.
Constrain each bit to be ∈ {0, 1}.
Constrain the sum of bits * 2^i to equal the input.

If any of these is missing or weak, an attacker can construct a “bit” that’s neither 0 nor 1 — for example, bit = 2. Suddenly the bit-array represents a value with more “weight” than n bits should encode, and downstream uses (like range checks or hash inputs) get the wrong semantics.

Bug pattern: a custom hand-rolled bit decomposition that constrains only the sum (Σ bᵢ · 2^i == n) but doesn’t constrain each bᵢ ∈ {0, 1}.

// Vulnerable: missing the per-bit boolean constraint
template BadBits(n) {
    signal input in;
    signal output bits[n];

    var sum = 0;
    for (var i = 0; i < n; i++) {
        bits[i] <-- (in >> i) & 1;   // unconstrained assignment!
        sum += bits[i] * (1 << i);
    }
    sum === in;                       // sum-of-bits constraint only
    // MISSING: for each i, bits[i] * (bits[i] - 1) === 0
}

Without the per-bit constraint, the prover can submit bits[0] = 5, bits[1] = -2 (in field arithmetic) and the sum still equals in. Downstream code that treats bits[i] as a 0/1 selector now does the wrong thing — possibly bypasses access controls or doubles up rewards.

Fix in circomlib’s standard Num2Bits:

for (var i = 0; i < n; i++) {
    out[i] <-- (in >> i) & 1;
    out[i] * (out[i] - 1) === 0;     // ← THE critical constraint
    lc1 += out[i] * e2;
    e2 = e2 + e2;
}
lc1 === in;

Audit move: when you see hand-rolled bit decomposition (or any “decomposition” pattern), check that each part is constrained to its claimed domain.

4.5 Sub-pattern 3: missing zero-check / division-by-zero

ZK circuits over a prime field have division (multiplication by inverse). If the divisor is zero, the inverse doesn’t exist, and any “result” the prover supplies is unconstrained.

template BadDivide() {
    signal input a;
    signal input b;
    signal output q;

    q <-- a / b;        // hint
    q * b === a;        // constraint
}

If b == 0, the constraint becomes q * 0 === a ⟹ 0 === a ⟹ a == 0. So when a == 0 and b == 0, any q satisfies. The circuit “verifies” a witness with arbitrary q. If q is used downstream as, say, a balance update, the prover picks the maximally favorable q.

Fix: add a non-zero check on b:

component isz = IsZero();
isz.in <== b;
isz.out === 0;          // assert b != 0

4.6 Sub-pattern 4: nondeterminism (multiple valid witnesses for the same input)

A deterministic circuit: for every (public_input, private_input), there is exactly one witness assignment satisfying the constraints. A nondeterministic circuit: for some input, multiple witnesses satisfy.

Nondeterminism is a soundness smell, even when no obvious exploit is apparent, because:

The circuit’s “meaning” is ambiguous.
An attacker can use the freedom to pass downstream checks that they shouldn’t.
Composition with other circuits may break.

// Constraint: x * y == z
// If z is the public input, prover can choose any factor pair (x, y).
// If x is also public, y is forced. If neither, the choice is the attacker's.

Audit move: pick a few public inputs and ask “given just these, how many witnesses satisfy the constraints?” If the answer is “many, depending on the prover’s choice”, that’s not necessarily a bug — but if any of those choices leads to a downstream semantic violation, it is.

The Aztec Connect 2022 bug ([verify] — Aztec disclosed several early circuit issues) involved a non-determinism in note creation that, in a specific code path, let a malicious note be valid in two different “shapes”. Recursive composition then accepted one shape on one layer and another on another.

4.7 Sub-pattern 5: signed/unsigned confusion + field-size confusion

Finite fields commonly used in 2026:

BN254 / BN128 scalar field: p ≈ 2^254 (used by Ethereum’s pairing precompiles, Groth16-on-Ethereum standard)
BLS12-381 scalar field: p ≈ 2^255
Goldilocks: p = 2^64 - 2^32 + 1 (used by Plonky2 / Plonky3)
Mersenne31 / BabyBear: small fields for Plonky3 and the SP1 ecosystem

The field size matters because:

Solidity uint256 is bigger than BN254’s scalar field. A Solidity-side input of 2^254 + 1 will be reduced mod p when passed to the verifier. If the on-chain caller doesn’t pre-constrain the input, two different uint256 values can map to the same field element, allowing an attacker to substitute. This is a frequent on-chain integration bug even when the circuit itself is fine.
Plonky2’s Goldilocks field is small enough that some “natural” range checks become trivial / unnecessary. Bug shape: the developer copies a Circom pattern that includes a range check for 64-bit safety; in Goldilocks the check is automatic but the developer adds a spurious extra constraint. Less catastrophic, more confusion.

Audit move on the boundary: every public input that is a Solidity uint256 and lands in the circuit must be require(input < FIELD_MODULUS) on the caller side, or the circuit must explicitly accommodate both reductions. Otherwise: two distinct on-chain inputs verify the same proof.

4.8 Mini-catalog: real-world ZK bugs and which pattern they fit

The 0xPARC ZK Bug Tracker is the authoritative source. A sampler (read the tracker entries themselves for full detail):

Bug name (approximate)	Pattern	Where
Semaphore — early identity-nullifier non-binding	Public-input binding (sub-class of under-constraint)	Semaphore v1.x [verify dates]
Tornado Cash — historic note hash collision (theoretical)	Hash-input encoding	Discussed publicly; mitigated
Aztec Connect — note-shape nondeterminism	Sub-pattern 4	Disclosed 2022 [verify]
zkSync — prover constraint bug (2023)	Field-size / encoding	Disclosed; patched [verify exact CVE]
BigUInt / BigInt circomlib templates — historic underflow	Sub-patterns 1, 2	Past circomlib versions; audit logs
Worldcoin / World ID — early identity circuit issues	Under-constrained nullifier checks [verify]	Disclosed in security reviews
Polygon zkEVM — main prover patches	Combined field/encoding	Multiple historical advisories
Reclaim Protocol — TLS-attestation circuit	Public-input binding	2024 audit reports

Lesson from the catalog: no single bug is “exotic”. Each is one of the five patterns above, applied to a specific application. The pattern recognition is the trainable skill.

5. The Other Bug Classes — what to look at when the circuit is “fine”

The circuit can be perfectly constrained and the system can still be exploited. Five non-circuit bug classes you, as a generalist auditor, are well-positioned to find.

5.1 Verifier contract bugs (Solidity-side)

The on-chain verifier is a Solidity contract auto-generated by the proof system’s tooling (e.g., snarkjs for Groth16). It looks like this (sketch):

contract Verifier {
    function verifyProof(
        uint256[2] calldata a,
        uint256[2][2] calldata b,
        uint256[2] calldata c,
        uint256[N] calldata input
    ) external view returns (bool) {
        // Pairing checks against the verification key (VK)
        // ...
    }
}

The auto-generated code is mostly trusted — most Groth16 verifiers are mechanically derived from the same template, and bugs at the pairing-check level are extraordinarily rare. Where bugs come in is the integration around the verifier:

Hardcoded verification key: the VK encodes the circuit; if the team upgrades the circuit but forgets to redeploy the verifier, proofs for the new circuit don’t verify against the old VK. Conversely, if the VK is upgradeable but the upgrade authority is weak, a malicious upgrade replaces the circuit silently.
No bound on input.length (or the calldata layout is fixed, but the caller passes the wrong number of elements): some integrations use a wrapper that passes a dynamic bytes to be decoded — wrong length → memory corruption or revert in odd places.
Field-modulus check missing on inputs: as in §4.7, the on-chain caller must require(input[i] < FIELD_MODULUS) for each public input. Some auto-generated verifiers do this internally; some don’t. Trust but verify.
No replay protection: nothing in the verifier itself prevents the same (a, b, c, input) tuple from being verified twice. If the calling contract’s action is non-idempotent (mint, transfer, vote), it must include a nullifier in the public inputs and track used nullifiers on-chain.

5.2 Public-input handling (the integration boundary)

This is the bug class generalist auditors find most often when reviewing ZK protocols. Pattern: the circuit attests to a statement that includes some public input — recipient, amount, nullifier, merkleRoot — and the on-chain caller passes (or fails to enforce) the right values.

Worked example: a withdraw circuit attests to “I know a preimage of a leaf in merkleRoot, and the recipient of the withdrawal is recipient”.

function withdraw(
    bytes32 nullifier,
    bytes32 merkleRoot,
    address recipient,
    uint256[8] calldata proof
) external {
    require(!spent[nullifier], "double-spend");
    require(isKnownRoot(merkleRoot), "unknown root");
 
    uint256[3] memory input;
    input[0] = uint256(nullifier);
    input[1] = uint256(merkleRoot);
    input[2] = uint256(uint160(recipient));   // ← (A)
    require(verifier.verifyProof(/*...*/, input), "bad proof");
 
    spent[nullifier] = true;
    payable(recipient).transfer(1 ether);     // ← (B)
}

Things to scrutinize:

Public input order: do positions in the Solidity input array correspond to the circuit’s public-input order? Mismatch = the proof “verifies” against semantically wrong values.
Field-modulus reduction: recipient is a 160-bit address packed into a 256-bit slot, then reduced into a ~254-bit field element. Multiple Solidity recipients could conceivably map to the same field element (only theoretical for an address smaller than the field, but the same pattern with larger values causes real bugs).
Binding (A) to action (B): the proof attests to some recipient, but does the contract send to that recipient? If between (A) and (B) the contract reads a different variable for the transfer target, the proof’s recipient is decorative.
merkleRoot freshness: a stale root might be a valid past root, allowing replay of an old proof. The isKnownRoot check must reject roots beyond some staleness window — but not so strict that legitimate users can’t withdraw.
nullifier collision: nullifier is a hash of some preimage; the preimage must be unique per note. If the circuit lets two different notes produce the same nullifier, double-spend.

5.3 Trusted-setup compromise

For Groth16 specifically — and to a lesser extent for KZG-based PLONK universal setups — the trusted setup ceremony produces parameters using random secrets. If all ceremony participants colluded to retain the secrets (“toxic waste”), they can forge proofs for the corresponding circuit indefinitely. One honest participant deleting their secret is enough to prevent forgery (the “1-of-N honest” assumption).

Audit angles:

Ceremony transcript published? Each participant publishes a contribution, signed. If you can’t enumerate participants and verify the contribution chain, the assumption is unverifiable.
Participants known and reputable? A ceremony of 5 employees of one company is technically valid but practically the same as a single party for risk purposes.
Phase 2 (circuit-specific) ceremony performed correctly? Groth16 has a circuit-agnostic Phase 1 and a circuit-specific Phase 2. The Phase 2 transcript matters per-deployment.
Re-keying after circuit changes? If the circuit changes even slightly, the Phase 2 must be redone.

The Powers of Tau ceremony (Filecoin / Hermez / many others) is the prevailing Phase 1 source for BN254 in 2026. Verify your protocol uses an audited Phase 1 base and a properly run Phase 2.

For transparent setups (STARK, IPA-Halo2): this bug class doesn’t apply. One reason to prefer transparent setups when feasible.

5.4 Recursive composition pitfalls

Already touched in §2.4. Specifically for audits:

Public-input flow across the composition boundary: a proof of “I verified an inner proof” must explicitly bind the inner proof’s public inputs into the outer proof’s public inputs. Missing this is the canonical recursive bug.
Trusted-setup compatibility: if the inner uses Groth16 and the outer uses Halo2, the curves must be compatible (e.g., the BLS12-377 / BW6-761 pair). Wrong curve choice = the wrapper can’t verify the inner soundly.
Recursion depth limits: some accumulation schemes have practical depth limits before soundness erodes. Spec should state the bound; implementation should enforce it.

5.5 Off-chain prover and key-management infrastructure

The prover is often the only party that can compute proofs at all (because the proving key for Groth16 is huge — multiple GB — and reasonable to keep on a prover machine). If the prover infrastructure is centralized:

Liveness: if the prover goes down, the system halts. Bridges relying on the proof can’t pay out.
Censorship: the prover can refuse to prove specific users’ transactions.
Selective proving: the prover proves transactions in an order that maximizes their MEV.
Key compromise: if the proving key is leaked, anyone can produce proofs — but this isn’t strictly a soundness issue (the proving key only lets you prove true statements; it’s the verification key that, if forged via toxic waste, lets you prove false statements). However, in some advanced schemes (Plonky2 with specific configurations), prover-key abuse opens additional doors.

Audit move: ZK rollups in 2025–2026 are mostly single-prover. Document this as an availability / censorship risk; flag any claim of “decentralized proving” as a thing to verify on-chain rather than take on trust.

6. Audit Workflow for a ZK-Adjacent Protocol

You’re handed a protocol that uses ZK. You’re not the circuit specialist. Here’s the workflow.

6.1 Step 1: Read the spec

The spec should state:

The predicate the circuit proves, in plain language. Something like: “Given a Merkle root R, a nullifier n, and a recipient a, the prover knows a leaf L in the tree rooted at R such that n = H(L, secret) and L has not been spent (encoded by the nullifier check).”
Public inputs vs private witness, exhaustively.
Proof system + curve + setup model, e.g., “Groth16 over BN254 with a Phase 2 from the published ceremony at https://…“.
On-chain integration: which contract calls the verifier, with what inputs, doing what action upon success.

If the spec is missing any of these, the spec is a finding by itself. Refuse to audit until they exist.

6.2 Step 2: Map signals to constraints (or read the audit report)

For each input/output signal, list:

What domain it’s supposed to live in (e.g., 32-bit unsigned, address, hash digest).
Which constraint enforces that domain.
If no constraint enforces it: that’s the under-constraint smell. Note it.

For Halo2 / Plonky2 / Cairo: you defer this to a specialist. But you produce the list of what to check, even if you don’t run the check.

6.3 Step 3: Identify constraints NOT present

This is the hard intellectual move. You’re trying to find what’s missing. Heuristics:

For every loop, every recursive structure, every “bit”, every “range”: is there a constraint enforcing the structural property? (Length, bit-boolean-ness, range fits.)
For every division / inverse: is the divisor constrained to be non-zero?
For every “amount” or numeric input: is it bounded?
For every public input: is it bound to the action the on-chain caller performs?
For every hash input: is the encoding canonical (no padding ambiguity, no length-extension)?
For every nullifier / unique identifier: is the binding to the underlying secret tight enough to prevent collisions?

You will not catch them all. You will catch enough to know when to escalate.

6.4 Step 4: Cross-check public inputs against on-chain expected use

You did this exercise for §5.2. Make it your default for every ZK protocol you audit. Trace each public input from the circuit through the verifier to the on-chain action. Flag any divergence.

6.5 Step 5: Look at the tooling and CI

A protocol with mature ZK security practices will have:

Static analysis (circomspect, Picus, Coda, Ecne for Circom; specific tools for Halo2/Noir) in CI.
A test suite that runs the prover-verifier roundtrip for many inputs, including adversarial inputs.
Fuzzing of the circuit constraints (Picus-style or custom).
A reference implementation in a high-level language (Python, Rust) against which the circuit output is compared.

The absence of any of the above isn’t a finding by itself, but it’s a strong signal of immaturity. Recommend each in your report.

6.6 Step 6: Document the trust assumptions

In your final report, the “Trust Assumptions” section should explicitly state, for the ZK component:

Soundness assumption: “We assume the circuit C is sound — i.e., any proof that verifies corresponds to a valid (public, witness) pair under the application’s intended semantics. This assumption is contingent on a circuit-specific audit by [Veridise / Zellic / etc.], which we recommend and have not performed.”
Setup assumption: “We assume the Phase 1 Powers of Tau ceremony was honest (1-of-N participant deleted toxic waste), and we have verified the Phase 2 ceremony performed by [team] involves [N] participants and is published at [URL].”
Verifier-contract assumption: “We assume Verifier.sol is correctly generated from the circuit-specific verification key and has not been tampered with post-deployment. We have verified this against snarkjs-generated output.”

Putting these in writing matters because:

It makes the protocol team explicitly acknowledge them.
It scopes your liability (you didn’t audit the circuit; you said so in the report).
It gives users a clear list of what would have to fail for them to lose funds.

This is the same discipline you use for bridge audits — make the trust seams explicit.

7. Tooling

A pragmatic 2026 tooling map.

7.1 Under-constraint detection

Tool	Maintainer	Status	Focus
Picus	Veridise	Active	Circom under-constraint detection via SMT
Coda	Veridise	Active	Coq-style formal verification for Circom
circomspect	Trail of Bits	Active	Static analyzer for Circom — code-smell and common-bug detector
Ecne	Privacy & Scaling Explorations	Active (research-grade)	R1CS-level analysis; checks if all signals are uniquely determined by the constraint system
gnark-pure-verifier checks	ConsenSys	Active	For gnark circuits; bounded testing

circomspect is the easiest to start with. It runs on Circom source, reports warnings like “signal not constrained”, “unused signal”, “side-effect-free assignment”. You will run it in §8.

Picus is heavier-weight, requires SMT setup, but actually detects under-constraints in many real cases. Investing time here pays off if you’re doing ZK audits regularly.

7.2 Halo2 / Noir / Plonky2 specific

Halo2: tooling is less mature for static analysis. The dominant practice is testing with the MockProver (which gives precise error messages on constraint violation) plus property-based testing of the circuit logic against a reference implementation.
Noir: nargo test framework includes constraint-soundness assertions; formal verification work is ongoing (Aztec has published on this).
Plonky2 / Plonky3: testing-heavy; tooling for static analysis is research-grade in 2026.

7.3 General

Reference implementations: write the predicate in Python or Rust; run both the proof system and the reference; assert agreement on adversarial inputs.
Property-based testing (Hypothesis, proptest): generate adversarial witnesses, prove, verify, assert what the application expects.
Coverage: many ZK circuits have low test coverage of edge cases. A finding-class on its own: “test suite covers fewer than X% of code paths; consider expanding.”

8. Lab

Three exercises. Together they take 4–8 hours depending on prior comfort.

8.1 Environment setup

# Node + npm
node --version  # need >= 18
 
# Circom (Rust-based compiler)
git clone https://github.com/iden3/circom.git ~/tools/circom
cd ~/tools/circom && cargo build --release
# add target/release/circom to PATH
 
# snarkjs (proof-generation utility)
npm install -g snarkjs
 
# circomspect (Trail of Bits static analyzer)
cargo install circomspect
 
# Lab directory
mkdir -p ~/web3-sec-lab/wk-bonus-zk && cd ~/web3-sec-lab/wk-bonus-zk

If your environment is finicky (Rust toolchain mismatch, snarkjs version drift), use the Docker image iden3/circom as a fallback. The exact commands above are [verify] against the current Circom release.

8.2 Exercise 1 — Read `IsZero`, identify what missing constraints would permit

Create IsZero.circom:

pragma circom 2.1.6;

template IsZero() {
    signal input in;
    signal output out;
    signal inv;

    inv <-- in != 0 ? 1/in : 0;
    out <== -in * inv + 1;
    in * out === 0;
}

component main = IsZero();

Task A — analytic:

List the two constraints (out + in*inv == 1, in*out == 0).
By hand, prove that for in == 0, the only valid witness is out == 1, inv = anything. Note the inv freedom: this is acceptable nondeterminism because out is uniquely determined.
Prove for in != 0, out is uniquely 0.

Task B — what if we removed the === constraint?

Modify the file to remove in * out === 0;. Compile:

circom IsZero.circom --r1cs --wasm --sym

Construct a malicious witness where in = 5 and out = 1 (intended is out = 0). With only out + in*inv == 1, the prover picks inv = 0, getting out = 1. The system “verifies” IsZero(5) == 1. Show that the verifier accepts this proof (generate the proof, verify it).

Task C — what if we removed out <== -in*inv + 1 and replaced with out <-- ...?

Same analysis. The prover now has total freedom over out. Confirm via constructing an adversarial witness.

Discussion: the <-- is your enemy when used without surrounding ===/<== constraints. Every Circom audit should grep for <-- and verify each one is pinned down elsewhere.

8.3 Exercise 2 — Run `circomspect` on a buggy circuit

Create Range.circom:

pragma circom 2.1.6;

template RangeCheck(n) {
    signal input in;
    signal output bits[n];

    var sum = 0;
    for (var i = 0; i < n; i++) {
        bits[i] <-- (in >> i) & 1;
        sum += bits[i] * (1 << i);
    }
    sum === in;
    // MISSING: bits[i] * (bits[i] - 1) === 0
}

component main = RangeCheck(4);

Run:

circomspect Range.circom

Task A: read the output. Identify which warning corresponds to the missing boolean constraint. Note that circomspect won’t catch every under-constraint, but it catches well-known patterns.

Task B: produce an adversarial witness in which bits[0] = 5, bits[1] = -2, bits[2] = 0, bits[3] = 0, and the sum still equals the input. (Field arithmetic: pick in such that 5 - 2*2 = in, i.e., in = 1.) Confirm the proof verifies.

Task C: patch with bits[i] * (bits[i] - 1) === 0 inside the loop. Re-run circomspect, re-run the adversarial witness, confirm proof generation now fails (or the witness fails to satisfy constraints).

Discussion: this is the canonical sub-pattern 2 bug from §4.4. Encountered repeatedly in real protocols.

8.4 Exercise 3 — Read a real on-chain ZK verifier

Pick a Solidity verifier from a deployed ZK protocol. Suggested starting points (verify they’re still live in 2026):

Tornado Cash classic Mixer verifier (legacy): deployed on Ethereum mainnet; the verifier was a standard Groth16 contract. Search Etherscan for Verifier.sol on a Tornado Cash mixer address (e.g., 0.1 ETH pool: 0x12D66f87A04A9E220743712cE6d9bB1B5616B8Fc). View the implementation code.
Semaphore-based identity protocols (Worldcoin, Sismo, Anon Aadhaar): each has a public Verifier contract. Worldcoin’s WorldIDIdentityManager is one entry point; the verifier sits behind it.
A small ZK rollup or coprocessor: Axiom, Risc0’s Bonsai verifiers, etc.

Task A: Locate verifyProof(...) (or equivalent). Identify:

Number of public inputs.
Layout of the proof (Groth16 = a[2], b[2][2], c[2]; PLONK = different).
Which input[i] is what semantically — look at the calling contract’s verifyProof(...) invocation and trace what each value represents.

Task B: Find the calling contract (the one that calls verifier.verifyProof). For each public input:

Is there a require(input < FIELD_MODULUS) check on inputs that originate as Solidity uint256?
Is there a nullifier-tracking mechanism preventing replay?
Does the action the contract performs upon verifyProof(...) == true use the same values as those passed in input?

Task C: Write a one-page “public-input flow” diagram for the protocol. Identify any potential binding gap.

Discussion: this is the audit move you’ll repeat for every ZK-integrating protocol you audit. The circuit may be perfect, but if the on-chain caller doesn’t bind its action to the proof’s public inputs, the proof is decorative.

8.5 Stretch — Try Picus on a circomlib template

Install Picus per the Veridise repo instructions. Run it on a circomlib template you’ve never read (e.g., MultiMux1, Pedersen, Sign). Read its output. Even when Picus reports “looks fine”, going through the experience teaches you what kind of analysis is automatable. When it reports a potential issue, dig into the template to understand whether it’s a real bug or a tool false positive.

8.6 Expected outcomes

After this lab:

You can read a Circom template and articulate its constraint set.
You can construct an adversarial witness for a simple under-constrained circuit.
You can run circomspect and interpret its warnings.
You can read an on-chain ZK verifier and trace its public inputs to the calling contract’s action.

You are not a circuit auditor. But you are now a Web3 auditor who can responsibly scope, triage, and integrate-test ZK protocols.

9. ZK in Rollups — quick connect-back for Week 11

If you’ve done Tuan-11-L2-Rollup-Modular-Security, here is where this chapter directly connects:

9.1 The validity-proof bridge

ZK rollups publish proofs of correct state transitions to an on-chain verifier. The verifier contract is the gate to the bridge: if the proof verifies, the new state root is accepted, and L2-side withdrawals can be honored on L1. Every concern in §5 of this chapter applies to every ZK rollup’s bridge.

Specifically:

Public input binding: the proof’s public inputs typically include the previous state root, the new state root, and some commitment to the batch of transactions. If the bridge contract uses any of those values for downstream logic (e.g., to settle a particular withdrawal), the binding must be airtight.
Verifier upgradeability: if the rollup’s verifier contract is upgradeable by a multisig, a malicious upgrade can install a “verifier” that accepts arbitrary inputs as valid. Look at the upgrade authority. (L2Beat’s stages framework codifies this; a “Stage 2” rollup has substantial restrictions on this upgrade path.)
Circuit-bug response: if a soundness bug is found in the rollup’s circuit, what is the recovery process? Pause the bridge? Roll back? Wait out a security-council process? The protocol’s incident-response design is itself a finding.

9.2 Where to look on L2Beat

For any rollup, L2Beat’s risk table includes a “Proof system” entry. Read it as:

“Validity proofs” — there is a circuit + verifier. All concerns in this chapter apply.
“Validity proofs (under review)” or “Permissioned” — the verifier isn’t fully decentralized; a council can override. Capture in trust assumptions.
“Fraud proofs” — optimistic; not this chapter’s concern, but ZK is starting to appear in inner parts of fraud proofs (e.g., proving correctness of a single step in a multi-round dispute).

9.3 Hybrid systems

Some L2s use a ZK proof inside an otherwise-optimistic system (e.g., to compress fraud-proof games). Some L1s use ZK in their consensus or DA layer (Mina, certain Cosmos zones). Treat each hybrid as a composition of trust assumptions: enumerate them, audit each component to its specialist, and document the joining points (public-input flow, again).

10. ZK Identity — Worldcoin, Semaphore, and the bug shapes there

A second connect-back: ZK identity protocols deserve special mention because they touch a different threat model than DeFi.

10.1 The class of system

Semaphore (PSE) — anonymous signaling: prove “I’m in this group” without revealing which member you are. Used by many privacy-preserving voting and reputation systems.
Worldcoin / World ID — proof of unique humanity: a person’s iris is hashed into a private identity commitment; ZK proofs let them sign messages as “a unique human” without revealing which one.
Anon Aadhaar / zkPass / Reclaim — ZK proofs over an external attestation (Aadhaar government ID, an HTTPS-signed TLS transcript, a web2 OAuth response). Lets a user assert “I have such-and-such attribute” without revealing the underlying credential.
zkEmail — ZK proofs over DKIM-signed emails, used for authentication and as oracles of email-based facts.

10.2 Bug shapes specific to identity

Non-binding nullifier: a user can mint multiple nullifiers for the same identity, breaking the “unique signal” property. (See [verify] reports on Semaphore-derived schemes.)
Identity-commitment collision: two distinct users hash to the same identity commitment. In a Sybil-resistant system, this can be exploited (one human becomes two voters) or DoS’d (one human’s identity is locked because another has the same commitment).
External-attestation forgery: in zkEmail-style systems, the circuit verifies a DKIM signature. If the verification is loose (e.g., accepts unusual DKIM canonicalization variants), an attacker forges a “valid” email proof for an email the recipient never sent.
Public-input binding (yet again): the proof attests to “I’m a unique human”, but the on-chain action uses a separate wallet address. If the address isn’t bound into the proof, the proof’s uniqueness doesn’t bind to the address — multiple addresses share one identity.

10.3 Worldcoin in particular

Worldcoin’s World ID has had multiple public-disclosure events involving early-circuit issues and Orb-hardware concerns. The relevant audit angles for a generalist:

The circuit attests to membership in the set of registered iris-hash holders. Public inputs include the action’s nullifier and a “signal” (the message being signed). If the nullifier or signal isn’t properly bound, replay is possible.
The on-chain WorldIDIdentityManager is the entry point. Look at upgrade authority, root-history retention window, and signal-encoding rules.
The off-chain prover: World ID proofs are generated client-side; the proving key is public. Security relies on the verification key matching the deployed circuit. If a malicious verifier deployment changes the VK, all guarantees fail.

These are the same audit moves as for a DeFi protocol — adapted to the identity context. The point is that the generalist moves transfer; what changes is the application’s intended semantics (uniqueness, attribute, membership).

11. Anti-patterns Cheat Sheet

Add these to your master audit checklist. They sit alongside the regular checklist items from earlier weeks.

For circuits (review by you for triage; deeper review by specialist):

<-- (unconstrained assignment) not paired with a constraint that pins down the assigned signal.
Hand-rolled bit decomposition without per-bit boolean constraint.
Range checks via subtraction-without-bit-decomposition (signed/unsigned confusion in the prime field).
Division (q <-- a/b; q*b === a) without b != 0 check.
Hash inputs with non-canonical encoding (padding ambiguity, variable-length concatenation, missing domain separation).
Same nullifier derivable from two distinct preimages — break uniqueness invariant.
Custom (non-circomlib) implementation of primitives without explicit reasoning about completeness ∧ soundness.

For the on-chain integration:

No require(input[i] < FIELD_MODULUS) on Solidity-side public inputs.
Public input order/encoding mismatched between circuit and verifier call site.
Nullifier tracking missing in a contract that performs non-idempotent actions on verification.
Verifier contract upgradeable without rationale; upgrade authority not documented.
Hardcoded verification key in an upgradeable system without VK-rotation policy.
Action performed by the contract uses a different value than the one in the proof’s public inputs.
Replay across deployments / chains: proof doesn’t bind to chainid and verifyingContract analogues.
Stale Merkle root accepted indefinitely — root rotation policy missing.

For the trust model:

Trusted setup transcript unavailable / unverifiable.
Ceremony participant list opaque or all from one organization.
Phase 2 (circuit-specific) ceremony not redone after circuit change.
Prover is single-party without articulated liveness / censorship mitigations.
Recursive composition without clear public-input flow specification.
“Decentralized proving” claimed but not realized on-chain.

For the audit report itself:

Trust Assumptions section names the circuit-specialist audit you didn’t perform.
Scope explicitly excludes circuit-level review and recommends specialist follow-up.
Severity scales with the dependence: a circuit bug in a $1B bridge ≠ a circuit bug in a hobbyist game.

12. Trade-offs and Open Debates

Decision	Option A	Option B	Auditor’s view
Proof system for new ZK app	Groth16 (smallest verifier; per-circuit trusted setup)	Halo2 / PLONK / STARK (larger verifier; less / no setup)	For high-value bridges where on-chain gas matters, Groth16 is still 2026’s pragmatic default if the Phase 2 ceremony is taken seriously. For changing circuits or post-quantum concerns, prefer transparent setups.
Circuit DSL	Circom (mature, widely audited, but easy to under-constrain)	Noir (cleaner abstractions, smaller bug footprint, less audit maturity)	For new application circuits in 2026, Noir is the better default unless team has deep Circom expertise. Audit infrastructure is catching up.
Trusted setup model	Per-circuit Phase 2 (Groth16)	Universal Phase 1 with KZG (PLONK family)	Universal is better for protocols that evolve their circuits; per-circuit is fine for stable, one-shot deployments.
In-house circuit vs reuse circomlib / battle-tested libraries	Reuse	Custom	Reuse always, unless a careful argument for custom exists. Custom circuits are where >50% of public bugs live.
Prover decentralization	Single prover (current default)	Decentralized prover network	Single prover for liveness / cost; decentralized for censorship resistance and reduced single-point trust. Most rollups are single-prover in 2026; this is a stated roadmap item, audit it as a current weakness.
Audit coverage	”We audited the protocol” (vague)	“We audited the integration; circuits audited by [specialist]“	The second is honest and useful. The first is malpractice when the circuit isn’t actually reviewed.

13. Quiz (≥80% to advance)

Q: What are the three properties a ZK proof system should provide, and which one is most often the source of value-destroying bugs? A: Completeness (honest prover convinces verifier), Soundness (no false proof verifies except with negligible probability), Zero-knowledge (proof reveals nothing about witness). Soundness is the value-destroying one — under-constrained circuits violate it.
Q: In one sentence, what is an “under-constrained circuit”? A: A circuit whose constraints permit witnesses that the developer did not intend, so the proof verifier accepts inputs that violate the application’s semantics.
Q: Why does Groth16 have a “per-circuit” trusted setup but PLONK + KZG has a “universal” one? A: Groth16’s proving and verification keys are derived from the specific circuit’s R1CS structure; changing the circuit requires a new Phase 2 ceremony. PLONK with KZG uses a universal Phase 1 (Powers of Tau) that supports any circuit up to a maximum size; per-circuit work is non-ceremonial.
Q: A Circom developer writes inv <-- 1/in; out <-- 1 - in*inv;. What’s wrong? A: Both assignments are unconstrained (<-- doesn’t impose a constraint). The prover can choose any values for inv and out. Need <== or accompanying === constraints to pin the signals down.
Q: A circuit’s public inputs include recipient (an address). The Solidity verifier receives this as a uint256. What’s the boundary bug? A: The address is reduced mod the field’s prime when passed into the verifier. The Solidity caller must require(input < FIELD_MODULUS) or two different uint256 recipient values that map to the same field element can both verify against the same proof. Also: the on-chain action must use the same recipient value, not a separately-supplied parameter.
Q: What does “1-of-N honest” mean in the context of a Groth16 trusted setup? A: As long as at least one ceremony participant securely deletes their contribution (the “toxic waste”), the resulting setup is sound — no coalition can forge proofs. All participants must collude for the setup to be compromised.
Q: Distinguish the dominant bug class in a circuit-specific audit from the dominant bug class in an integration-level audit of a ZK protocol. A: Circuit-specific: under-constrained circuits (missing constraints permit unintended witnesses). Integration-level: public-input binding bugs (the on-chain caller doesn’t enforce the same values as the proof’s public inputs, or applies them to a different action than the proof attests to).
Q: When auditing a ZK rollup’s L1 bridge, name three things you check on the on-chain verifier contract. A: (i) Upgrade authority and the time/process to swap the verifier or VK. (ii) Layout and modulus-bounding of the public inputs. (iii) That the bridge’s withdrawal action is bound to the proof’s public inputs (state roots, nullifiers, etc.) rather than a separately-supplied parameter.
Q: A protocol advertises “post-quantum security” for its ZK proofs. They use Groth16 over BN254. Is the claim true? A: No. Groth16 over BN254 relies on the hardness of the discrete-log and pairing-related problems, which are broken by large quantum computers. Only STARK and similar hash-based systems are plausibly post-quantum.
Q: A protocol’s audit report says “We audited the contract.” The contract calls a Verifier.verifyProof(...). What’s missing from the report? A: Whether the circuit underlying the verifier was audited (and by whom), the trust assumptions about the trusted setup, the verifier-key provenance, and the public-input binding analysis between the proof and the on-chain action. A serious report names the boundary explicitly and either covers it or names the specialist who will.
Q: Why is Num2Bits(n)’s per-bit bits[i] * (bits[i] - 1) === 0 constraint critical? A: Without it, a “bit” can be any field element (e.g., 5, -2, or any non-{0,1} value). Downstream code that treats bits[i] as a boolean indicator or as a weighted summand can be made to behave arbitrarily, breaking range checks, selectors, and any logic depending on the bit’s truth value.
Q: Recursive proof composition: a proof π_outer attests to “I verified π_inner”. What public-input binding must exist between them? A: π_outer must include in its public input the exact public input that π_inner attested to. Otherwise an attacker can construct π_inner attesting to one statement while π_outer claims to have verified a different statement — composition is unsound.

14. Deliverables

Lab Exercise 1 — IsZero analysis: written walkthrough of constraint set, adversarial witness for the two ablation cases.
Lab Exercise 2 — circomspect output on the buggy range-check circuit, interpretation in your own words, patched version that passes.
Lab Exercise 3 — Public-input flow diagram for one real on-chain verifier of your choice, with at least one identified or hypothesized binding concern.
One-page memo: “If I were scoping an audit of a ZK protocol, here is how I would scope the circuit work, what I would carve out for a specialist, what I would do myself, and how I would write the trust-assumptions section.”
Anti-pattern checklist additions integrated into your audit-checklist-master.
(Stretch) Picus run on a circomlib template + writeup.

15. Where this leads

This chapter is a vocabulary investment, not a vocational pivot. After it:

If you audit DeFi protocols on a ZK rollup (Tuan-11-L2-Rollup-Modular-Security), you can articulate the additional trust assumptions imported by the rollup’s proof system.
If you audit a privacy / identity protocol, you can map its claims to the underlying circuit’s properties and demand specialist review where appropriate.
If you audit a bridge that uses a ZK light client, you can scope the off-chain prover, the verifier contract, and the bridge logic distinctly.
If you want to become a circuit auditor, this chapter is your launchpad; from here, deep-dive Circom, then a proof system of choice (Halo2 or Plonky2), then internship/apprentice with Veridise / ToB / Zellic / PSE Audits.

The next chapter to read depends on your trajectory:

For deeper formal-methods: Tuan-Bonus-Formal-Verification-Deep — Certora, Halmos, K framework. ZK and formal verification meet in many places (proving circuit equivalence to a reference implementation, SMT-solving constraint systems).
For competitive auditing: Tuan-Bonus-Audit-Competition-Playbook — ZK protocols increasingly appear in Code4rena / Sherlock contests; the integration-level moves above are directly applicable.
For non-EVM execution surfaces: Tuan-Bonus-Non-EVM-Solana and Tuan-Bonus-Non-EVM-CosmWasm-Move — Starknet (Cairo / STARK) lives in this neighborhood architecturally.

The general posture: ZK is the most rapidly growing source of “I don’t know what to audit here” anxiety for generalist Web3 auditors in 2026. You don’t fix that anxiety by becoming a cryptographer overnight; you fix it by knowing precisely where your competence ends, naming the specialist work that picks up there, and auditing the integration layer thoroughly. That integration layer is where the money is, and it is, perhaps surprisingly, also where most of the historical ZK losses have come from.

Last updated: 2026-05-16 See also: Roadmap · References · MOC-Web3-Security-Mastery · Tuan-01-Web3-Blockchain-Crypto-Fundamentals · Tuan-11-L2-Rollup-Modular-Security · Tuan-Bonus-Formal-Verification-Deep

lthieu's notes

Explorer

Tuan-Bonus-ZK-Circuit-Security