Auditing Circom Circuits: A Practical Walkthrough

Auditing a circom circuit is not like auditing a Solidity contract. There is no reentrancy, no gas griefing, no msg.sender confusion. There is essentially one question, asked hundreds of times: does the constraint system actually enforce the statement the developers think it enforces? This guide walks through a practical workflow for answering that question, in the order an experienced reviewer would actually work.

Step 1: Scope the Engagement Correctly

Before reading a line of circom, establish the boundary of the system:

Which circuits, at which commit? Pin a commit hash. Circuits change constraint semantics with one-character diffs (<-- vs <==).
Which compiler version and flags? Circom versions differ in optimizer behavior (--O0/--O1/--O2 can remove or rewrite constraints). Audit what will ship, compiled how it will ship.
What surrounds the circuit? The verifier contract, the public input handling, the proving key provenance, and the witness generation service are all in the trust boundary. A perfect circuit behind a verifier that doesn't validate public inputs is still broken. Agree explicitly on whether these are in scope; if not, say so in the report.
Which proving system? Groth16 via snarkjs is the common case; it brings trusted setup and proof malleability considerations that belong in the report even when the ceremony itself is out of scope.

Step 2: Reconstruct the Intended Statement

This is the highest-leverage step and the one most often skipped. Write down, in precise mathematical English, what the proof is supposed to mean:

"There exists a note commitment C in the Merkle tree with root R (public), such that the prover knows the opening of C to (amount, secret), the public nullifier N equals H(secret, leafIndex), and amount equals the public withdrawal amount, which is in [0, 2^64)."

If the team cannot produce this statement, producing it is the first finding — a circuit without a specification cannot be verified against anything. Every quantifier matters: "there exists," "equals," "in range." Each clause of the statement must map to identifiable constraints. Keep this document open for the entire audit; it is your checklist.

Step 3: Signal-by-Signal Constraint Review

Now read the circuit, but not top-to-bottom like prose. Work signal by signal:

Inventory the signals. For each signal input, signal output, and intermediate signal, note whether it is public or private, and what integer range and meaning it is supposed to have.
For each signal, ask: what constrains it? List the constraints it appears in. A signal that appears in zero constraints is attacker-controlled. A signal "constrained" only through another unconstrained signal is also attacker-controlled — trace transitively.
For each intended property, ask: which constraint enforces it? Range membership, booleanity, uniqueness of decomposition, equality to a hash output — every clause in the intended statement needs a named constraint. If you can't point at it, it doesn't exist.
Check component wiring. Instantiating component lt = LessThan(64) does nothing until inputs are wired and the output is constrained. lt.out === 1 is the enforcement; without it, the comparator is decoration. This "computed but unchecked flag" pattern is among the most common real findings.
Check public input binding. Every public input should be load-bearing. A public input that no constraint touches invites verifier-layer confusion, and in Groth16 systems each public signal must be validated on-chain (see Step 6).

Step 4: The `<--` Diff Review

Grep for every use of <-- (and -->). For each occurrence, demand a justification and a paired constraint:

// Pattern: assignment plus explicit constraint
quotient <-- in \ divisor;
remainder <-- in % divisor;
in === quotient * divisor + remainder;
// Still incomplete! Must also constrain:
//   remainder in [0, divisor)   -- else many (q, r) pairs satisfy it
//   quotient range              -- else field wraparound forges values

The division example above is the canonical trap: the equality constraint alone admits infinitely many satisfying pairs over the field. The range side-conditions are what make the decomposition unique. Apply this discipline to every <--: what set of values satisfies the paired constraints, and is that set exactly the intended one?

Also review === usage for expressions that could not compile as <== — a developer who split assignment and constraint may have constrained a subtly different expression than they assigned.

Step 5: Template Parameters and circomlib Pitfalls

Circom templates are parameterized, and constraints can degenerate at edge values:

Instantiate the extremes. What does LessThan(n) mean when n is large enough that 2^n approaches the field size? circomlib's LessThan is only sound when inputs genuinely fit in n bits — which the template itself does not enforce. The caller must range-check inputs first. This caller-side obligation is the classic circomlib pitfall.
Num2Bits vs Num2Bits_strict. At widths near 254 bits, non-strict decomposition is non-unique due to aliasing past the field modulus. Full-width decompositions must use the strict variant.
Loop bounds of zero. A template instantiated with a size parameter of 0 may generate no constraints at all while the parent assumes it validated something.
Signed semantics. Nothing in the field is negative. Any template documentation mentioning "negative numbers" deserves a careful read of what encoding is assumed.

Read the circomlib source for every imported template. It is short, and the comments state input assumptions that callers routinely violate.

Step 6: Tooling Passes

Run tools after manual review, not instead of it — their output means more once you know the circuit.

circomspect (Trail of Bits): flags unconstrained signals, <-- without nearby constraints, unused outputs, and shadowing. Triage every warning; suppress with written justification.
snarkjs r1cs info / r1cs print: check constraint and public input counts against expectations. Diff counts across versions of the circuit — a security fix that doesn't increase the constraint count is suspicious, and an optimizer pass that slashes it needs explanation.
Determinism checkers: run Picus on the circuit or its critical subcomponents to check that outputs are uniquely determined by inputs. Timeouts are common on large circuits; scope it to the gadgets that matter.
Witness fuzzing / negative testing: build harnesses that generate invalid witnesses — out-of-range values, mismatched nullifiers, wrong Merkle paths — assign them directly (bypassing the honest generator), and assert that proof verification fails. Honest-input tests cannot detect under-constraint by construction; only adversarial witnesses can.
Verifier-side checks: confirm the on-chain verifier validates that public inputs are canonical field elements and that the protocol handles Groth16 proof malleability (a valid proof can be re-randomized into a different valid proof for the same statement — never use the proof bytes as a nullifier or uniqueness key).

Step 7: A Findings Taxonomy That Maps to Fixes

Classify findings so engineers know what kind of fix is needed:

Under-constrained signal / missing constraint — soundness; usually critical.
Missing range check / aliasing — soundness; critical to high.
Unchecked component output — soundness; critical to high.
Public input not bound or not validated in verifier — soundness at the integration layer.
Over-constrained circuit — completeness: honest users can't prove valid statements; a denial-of-service, typically medium.
Privacy leakage — a public signal or verifier event reveals more than intended.
Specification gap — the intended statement is ambiguous or undocumented.

Reporting

For each finding, include: the intended property, the constraint that should enforce it, why it doesn't, and — wherever feasible — a concrete forged witness demonstrating exploitation. A proof-of-concept witness that verifies is unanswerable; it converts an argument about semantics into a reproducible failure. Close the report with the intended-statement document itself as an appendix, so the next audit starts from a specification instead of from zero.

Closing

Circom audits reward methodical paranoia over cleverness. Reconstruct the statement, account for every signal, distrust every <--, read the circomlib source, and prove exploitability with forged witnesses. The circuits that survive this process are the ones whose authors can answer, for every value in the system: what forces this?