sorryfreeLast reviewed 2026-09-13
Index › Glossary › Underconstrained circuit

Underconstrained circuit

Direct answerA circuit whose constraints admit witnesses outside the specification, typically because a value computed during witness generation is never pinned down by a constraint. It is the dominant class of exploitable ZK bug.

In more detail

In Circom the classic form is a <-- assignment without a matching === constraint; in Halo2 it is a cell that is assigned but not gated; in any system it is a missing range check, a missing boolean check or a division by a possibly-zero value. Automatic tools (Picus, CIVER, NAVe) detect many instances by checking that outputs are uniquely determined by inputs; a soundness proof rules out all of them.

Frameworks that address it

Picus, CIVER, Circomspect, zkFuzz, NAVe.

Circuit soundness, Circuit completeness, Overconstrained circuit, Symbolic vs computational model, Specification gap, Trusted computing base and verification boundary, Proof assistant vs SMT-based verifier, Bounded model checking, Equivalence checking, Refinement, Constant-time verification, Arithmetization (R1CS, PLONKish, AIR), Extraction (code to model), Witness generation vs constraints

Getting help

Firms on this index that handle this in practice: zkSecurity, Galois, Veridise, Nethermind (Formal Verification team).

Last reviewed 2026-09-13 by the sorryfree editors. Machine-readable: data.json · summary.txt