ZK Bug Classes: Under-Constrained Circuits

If you audit enough zero-knowledge circuits, one pattern dominates the findings list: the circuit computes the right answer for honest inputs, but never actually forces that answer. These are under-constrained circuits, and they are the ZK equivalent of missing access control in a smart contract. The prover is the adversary. Anything the constraint system does not explicitly forbid, a malicious prover is free to do.

Witness vs. Constraints: Two Different Programs

A circuit in a system like circom really describes two things at once:

• Witness generation — ordinary code that computes values for every signal, run by the prover on their own machine.
• The constraint system — a set of equations (in R1CS, of the form a * b = c over a finite field) that the verifier's checks ultimately enforce.

The verifier never sees your witness generation code. It only checks that the submitted witness satisfies the constraints. A malicious prover can throw away your witness generator entirely, hand-craft any assignment they like, and produce a valid proof — as long as the constraints are satisfied.

Circom makes this distinction syntactically explicit, and it is the single most important thing to internalize:

// Assignment ONLY — computes a value, adds NO constraint
out <-- in \ 4;

// Assignment AND constraint — but only valid for quadratic expressions
out <== in * scale;

// Constraint only, no assignment
out * 4 === in - remainder;

<-- exists because some computations (integer division, bit decomposition, modular inverse, hash preimages) cannot be expressed directly as a single quadratic constraint. The correct pattern is always: assign with <--, then separately constrain the result with ===. Every <-- that is not paired with a constraint that pins down the assigned value is a potential forgery vector.

Classic Under-Constraint Patterns

Missing range checks

Field elements are not integers. In a BN254 circuit, every signal lives in a field of roughly 2^254 elements. If your circuit treats a signal as "an 8-bit amount" but never constrains it to [0, 255], the prover can supply a value like p - 1, which behaves as -1 under field arithmetic. Balance checks, comparisons, and bit decompositions all silently break.

// BROKEN: nothing stops bits[i] from being any field element
signal input in;
signal output bits[8];
for (var i = 0; i < 8; i++) {
    bits[i] <-- (in >> i) & 1;
}

// FIXED: force booleanity and force recomposition
for (var i = 0; i < 8; i++) {
    bits[i] <-- (in >> i) & 1;
    bits[i] * (bits[i] - 1) === 0;   // each bit is 0 or 1
}
signal sum;
// sum of bits[i] * 2^i must equal in

Without the booleanity constraint and the recomposition constraint, bits is fiction.

Unconstrained outputs and dead signals

A template output that is assigned with <-- but never appears in any constraint is completely attacker-controlled. This also happens at the composition layer: a subcomponent computes a validity flag, and the parent circuit never checks it. Num2Bits from circomlib enforces its decomposition, but a comparator whose output you ignore enforces nothing about your business logic.

Aliasing and field overflow

Arithmetic in circuits wraps modulo the field prime p. Two dangerous consequences:

• Overflow: summing enough "small" values can exceed p and wrap, so a sum of positive amounts can equal a small number. Balance-conservation constraints must bound the number and size of operands.
• Aliasing: a 254-bit decomposition of a field element is not unique — some bit patterns represent values ≥ p that alias to small field elements. This is why circomlib ships Num2Bits_strict, which adds a comparison against the field modulus. Using the non-strict variant on full-width values is a recurring audit finding.

Bad nullifier and uniqueness constraints

Privacy protocols prevent double-spends with nullifiers: a deterministic value revealed on spend, derived from the note and a secret. Common failures:

• The nullifier is computed in witness generation but not constrained to the correct derivation, letting a prover mint arbitrary nullifiers and spend one note many times.
• The nullifier derivation omits an input (for example, the leaf index), so two distinct notes share a nullifier, or one note yields several.
• Public inputs feeding the nullifier check are not bound to the Merkle membership proof, so the "spent" note and the "proved" note can differ.

How These Bugs Are Exploited

The exploit shape is always the same and requires no cryptographic break. The attacker writes their own witness generator that satisfies the constraints while violating the intended statement — for example, a withdrawal proof for funds they never deposited, or a second spend of an already-spent note. The proof is genuinely valid: pairing checks pass, the verifier contract accepts it. From the chain's perspective, nothing anomalous occurred. This is what makes under-constraint so dangerous compared to contract bugs — there is often no on-chain signature of the attack beyond its economic effect, and soundness failures in shielded pools may be undetectable even after the fact.

Real incidents underline that this class is not theoretical. Zcash's original Sprout system used the BCTV14 proving system, which was later found to have a subtle flaw in how its parameters were generated that could have allowed counterfeiting of shielded ZEC; it was quietly fixed via the Sapling upgrade, and no exploitation was ever detected. Trail of Bits' "Frozen Heart" disclosures showed that multiple independent implementations of Fiat–Shamir-based protocols failed to hash enough of the transcript, making forged proofs possible — a soundness failure at the protocol layer rather than the circuit layer, but with the same outcome. And ChainLight reported a soundness bug in zkSync Era's proof system that could have allowed proving invalid blocks; it was responsibly disclosed and patched before exploitation. Relatedly, the 2022 BNB bridge exploit forged an IAVL Merkle proof accepted by a buggy verifier — not a ZK system, but the identical lesson: the verifier accepts whatever its checks fail to exclude.

Detection Approaches

No single tool closes this class. Layer them:

• Static analysis — circomspect. Trail of Bits' linter flags signals assigned with <-- but never constrained, unused outputs, and other suspicious patterns. Cheap to run in CI; expect false positives you triage once.
• Determinism / uniqueness checking — Picus. Picus attempts to verify that a circuit's outputs are uniquely determined by its inputs (i.e., the circuit is properly constrained), using SMT-based reasoning. Ecne pursued the same goal earlier for R1CS. These tools directly target the definition of under-constraint, though they can time out on large circuits.
• Formal methods. For high-value core components (hash gadgets, Merkle verification, nullifier derivation), a hand or machine-checked proof that the constraint system implies the intended statement is the strongest assurance available.
• Adversarial witness testing. Skip your witness generator: construct malicious witness assignments directly (via a modified generator or by editing the witness file) and check that snarkjs proof verification fails. Every negative test that passes verification is a live vulnerability. Most test suites only test honest witnesses, which by construction cannot find under-constraint.
• Constraint-count review. snarkjs r1cs info gives constraint counts. A "range check" template contributing zero constraints, or a refactor that drops the count unexpectedly, deserves scrutiny.

Takeaways

• Treat every <-- as a claim requiring a matching constraint; review them as diffs the way you review unsafe blocks in Rust.
• Assume the prover discards your code and hand-writes witnesses. Ask, signal by signal: what forces this value?
• Range-check everything that models an integer; use strict decompositions at full field width.
• Bind nullifiers, Merkle roots, and public inputs to each other explicitly.
• Put circomspect in CI, run Picus on what it can handle, and build a negative test suite of forged witnesses that must fail verification.

Under-constrained circuits are the default state of a circuit under development. Soundness is something you add, constraint by constraint — and verify adversarially.