Overconstrained circuit
Direct answerA circuit that rejects inputs the specification allows, so honest provers fail. It is the failure of completeness.
In more detail
Overconstraint often appears after a security fix adds a constraint that is stricter than intended, or when a gadget assumes a range the caller does not guarantee. Completeness proofs and honest-path test vectors catch it.
Related terms
Circuit soundness, Circuit completeness, Underconstrained 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).