Circuit soundness
In more detail
Soundness is the property that rules out underconstrained circuits, and it is what most ZK verification efforts prove first. Because the adversary chooses the witness, a soundness argument must consider every satisfying assignment, not only the ones an honest witness generator produces.
Soundness alone is not enough: a circuit with no satisfying assignments is vacuously sound. That is why Clean and zk.golf require completeness alongside it, and why a soundness-only theorem should be read together with tests showing the circuit accepts honest inputs.
Frameworks that address it
Related terms
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), Witness generation vs constraints
Getting help
Firms on this index that handle this in practice: zkSecurity, Galois, Veridise, Nethermind (Formal Verification team).