Underconstrained Circuits: The Most Common ZK Bug, Explained

Video transcript

An underconstrained circuit accepts values your honest code would never produce. So a prover can prove something false, and the proof still verifies.

The verifier only checks constraints, so a malicious prover can skip your witness code and pick any values that satisfy them.

A 2024 study of 141 real vulnerabilities found 95 of the 99 circuit-layer bugs were underconstrained.

In Circom, the arrow with equals signs assigns and constrains. The dashed arrow only assigns, so a prover can change it unless another constraint pins it.

Real incidents follow three patterns. Circomlib's MiMC hash left its output unconstrained, Dark Forest and ZK Email missed range checks, and missing logic let a zkEVM circuit return 8 instead of 4.

Circom's inspect flag and Trail of Bits' Circomspect warn on risky patterns. Veridise's Picus and Ecne try to prove outputs are unique, but either can fail to decide.

Tools catch mechanical gaps. But wrongly translated logic, the largest root cause, needs a reviewer who knows what the circuit should prove.

Default to the constraining operator, range-check inputs with Num2Bits, and constrain divisors to be non-zero. Then write negative tests and run Circomspect on every change.

Your verifier contract is smart contract code too. Read the full article, or talk to Guardian about the code around your proofs.

A zero-knowledge proof is only as strong as the circuit behind it. The verifier checks the constraints, and nothing else.

If a constraint is missing, a prover can satisfy the rest with values the honest code would never produce. The proof still verifies.

That gap is an underconstrained circuit. A 2024 study of 141 real vulnerabilities found it to be the most common bug class in ZK circuits.

What Underconstrained Means

A circuit has two halves. Witness code computes the values; constraints are the equations a valid proof must satisfy.

An honest prover runs your witness code. A malicious one does not have to, and can pick any values that satisfy the constraints.

The 0xPARC zk-bug-tracker defines underconstrained circuits as those that "do not have all of the required constraints necessary to force proof makers to follow the intended rules".

The result is a soundness bug. Depending on what is missing, a prover can forge a hash output, mint a second nullifier for one note, or underflow a balance.

In the SoK by Stefanos Chaliasos and co-authors, 95 of the 99 circuit-layer bugs were underconstrained. Their root causes:

Trail of Bits' Circomspect docs agree: under-constrained signals "are one of the most common issues in zero-knowledge circuits."

Assigned vs Constrained

In Circom, some operators add constraints and some only assign values. One character separates them:

Circom's docs call <-- "dangerous" and say it should generally be paired with ===. Their example:

a <-- b/c;
a*c === b;

Division is not a quadratic constraint, so the value is assigned and then checked by multiplication.

Even this has a gap. Circomspect warns that the check can pass when the divisor is zero, so c needs its own non-zero constraint.

Halo2 has the same trap in another shape. Constraints live in configure and values in assign, so correct assignments can hide a missing constraint.

Three Real-World Patterns

1. Assigned, not constrained: circomlib MiMC

The circomlib MiMCSponge template set its output with =, which added no constraint, instead of <==. Kobi Gurkan's one-line fix was merged on September 17, 2019.

Until then, a prover could choose the hash output. The 0xPARC tracker says Tornado Cash's circuits used this hash, so an attacker could fake a Merkle root and withdraw other users' ETH.

2. Missing range checks: Dark Forest and ZK Email

The circomlib LessThan(n) template assumes both inputs fit in n bits. It does not enforce that.

Dark Forest v0.3 built a range proof on it without bit-length checks, so out-of-range values could pass. The fix added Num2Bits checks on the inputs.

The pattern returned in 2024. Matter Labs' red team found that ZK Email's regex circuits used byte 255 as a start marker, without range-checking user input.

An attacker could put \xff and a victim's address in an email subject, and the circuit would read it as the sender. A November 2024 fix range-checks every input byte.

3. Missing logic: PSE zkEVM and MACI

A January 2023 issue showed that the PSE zkEVM's SHL opcode circuit never constrained shf0 to be the first byte of shift.

A malicious prover could make 2 1 SHL return 8 instead of 4. The values were assigned correctly; the constraint was missing.

In MACI 1.0, the coordinator could apply a vote to the wrong public key, mark it invalid and so censor it. The fix was tracked in a December 2021 issue.

Not every forged proof is underconstrained

Zcash's counterfeiting flaw, disclosed on February 5, 2019, sat in the BCTV14 proving system's parameter setup, not in a circuit.

Electric Coin Company says the Sapling upgrade closed it on October 28, 2018, and that it believes no counterfeiting occurred.

Tools That Find Them

Each has limits. Picus answers safe, unsafe or unknown, and unknown means manual review or a longer solver timeout.

Ecne's README notes that a false result "does not mean that the constraints aren't sound", only that Ecne could not prove them.

The SoK adds that SMT-based tools such as Picus struggle with finite field arithmetic.

Tools catch mechanical gaps. A circuit that faithfully constrains the wrong logic, the largest root cause above, needs a reviewer who knows what it should prove. See how to find critical vulnerabilities.

For where proofs, fuzzing and manual review each fit, see formal verification vs fuzzing vs audit.

Prevention Checklist

1. Default to <==. Justify every <-- with the constraints that pin it.
2. Compile with --inspect and treat each warning as a question.
3. Range-check inputs to LessThan and similar templates with Num2Bits.
4. Use Num2Bits_strict when an input can reach the field size.
5. Constrain every divisor to be non-zero.
6. Constrain every public input; Circom's optimizer can drop unused ones.
7. Make nullifiers deterministic: one note, one nullifier.
8. In the verifier contract, require public inputs below the field modulus.
9. Write negative tests: hand-built witnesses that must fail.
10. Run Circomspect on every change, and Picus on core templates.

Where Guardian Fits

A ZK application is more than its circuit. The verifier contract and the state it updates are smart contract code.

A Guardian smart contract audit runs in three passes: design review, an invariant suite around core safety properties, and manual review by senior researchers.

A Vanguard audit adds a $100,000 Guardian-funded contest, a hosted bug bounty with $50,000 in Critical matching, and six months of update review.

Frequently Asked Questions

What is an underconstrained circuit?

It is a ZK circuit whose constraints accept witnesses the intended computation would never produce. A malicious prover can choose those values and the verifier still accepts the proof, so a false statement can be proven.

What is the difference between <-- and <== in Circom?

The <== operator assigns a value and adds a constraint, so every valid proof must respect it. The <-- operator only assigns during witness generation. A prover can replace that value unless separate === constraints pin it down.

Can tools find every underconstrained bug?

No. Circomspect flags known patterns. Picus and Ecne try to prove outputs are uniquely determined, but either can fail to decide. A circuit that faithfully constrains the wrong logic still needs a reviewer who knows what it should prove.

Was the Zcash counterfeiting bug an underconstrained circuit?

No. Electric Coin Company traced it to the parameter setup of the BCTV14 proving system, which produced extra elements that allowed false proofs. The 0xPARC zk-bug-tracker files it as a trusted setup leak.

Sources

• Chaliasos et al.: SoK: What Don't We Know? Understanding Security Vulnerabilities in SNARKs (arXiv, 2024)
• 0xPARC on GitHub: ZK Bug Tracker
• Circom Docs: Constraint Generation
• Circom Docs: Improving security of circuits with the --inspect option
• Trail of Bits on GitHub: Circomspect
• Trail of Bits: Circomspect analysis passes
• Veridise on GitHub: Picus
• Franklyn Wang on GitHub: Ecne, an engine for verifying the soundness of R1CS constraints
• iden3 circomlib: PR #22, mimcsponge fixes assignment to outs[0] (September 17, 2019)
• Dark Forest on GitHub: range proof fix commit
• Matter Labs: ZK Email, Unveiling Classic Attacks and Why Zero-Knowledge Proofs Alone Are Not a Panacea (November 2024)
• ZK Email zk-regex: input range check fix (November 7, 2024)
• PSE zkevm-circuits: Issue #1124, Soundness Bug: SHL Opcode Missing Constraint (January 31, 2023)
• PSE MACI: Issue #320, Fix MACI 1.0 ProcessMessages circuit to prevent message censorship (December 1, 2021)
• Electric Coin Company: Zcash Counterfeiting Vulnerability Successfully Remediated (February 5, 2019)
• Guardian: Smart Contract Audit
• Guardian: Vanguard