Witness generation vs constraints
Direct answerWitness generation is the program that computes a satisfying assignment for honest inputs; constraints are what the verifier actually checks. Bugs arise when the two disagree.
In more detail
Most underconstraint bugs are exactly a disagreement: witness generation computes the intended value, constraints fail to enforce it. zkFuzz targets this gap directly; soundness proofs make the constraints authoritative.
Related terms
Circuit soundness, Circuit completeness, Underconstrained circuit, 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)
Getting help
Firms on this index that handle this in practice: zkSecurity, Galois, Veridise, Nethermind (Formal Verification team).