Glossary
Direct answerShort, precise definitions of the terms that decide whether a formal verification result means what it appears to mean: circuit soundness and completeness, underconstrained circuits, symbolic vs computational models, specification gaps, the trusted computing base, proof assistants vs SMT verifiers, bounded model checking, equivalence checking and refinement.
- Circuit soundness
- A circuit is sound with respect to a specification if every witness that satisfies its constraints also satisfies the specification, so a malicious prover cannot produce an accepting proof of a false statement.
- Circuit completeness
- A circuit is complete with respect to a specification if every input the specification allows has a satisfying witness, so an honest prover is never blocked from proving a true statement.
- Underconstrained circuit
- A 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.
- Overconstrained circuit
- A circuit that rejects inputs the specification allows, so honest provers fail. It is the failure of completeness.
- Symbolic vs computational model
- The symbolic (Dolev-Yao) model treats cryptographic primitives as perfect black boxes and searches for logical attacks automatically; the computational model reasons about probabilistic polynomial-time adversaries and concrete security bounds, matching cryptographers' proofs.
- Specification gap
- A mismatch between the property that was formally proved and the property that was actually needed, so a valid proof fails to cover real behaviour.
- Trusted computing base and verification boundary
- Everything that must be correct for a proof to mean what it claims: the prover kernel, the axioms used, the extraction or translation from code to model, the specification itself, and any unverified glue code. The edge of that set is the verification boundary.
- Proof assistant vs SMT-based verifier
- A proof assistant (Lean, Rocq, Isabelle, F*) checks human- or AI-written proofs against a small kernel and can express arbitrary mathematics; an SMT-based verifier (Picus, CIVER, Certora Prover, Kani) discharges properties automatically but only within decidable fragments and may return 'unknown'.
- Bounded model checking
- Exhaustive exploration of all program executions up to a fixed depth or loop bound, reporting concrete counterexamples; sound only within the bound.
- Equivalence checking
- Proving that two artifacts compute the same function, for example optimised assembly against a Cryptol reference, or the KEVM semantics against a Lean EVM model.
- Refinement
- A relation showing that an implementation's behaviours are a subset of a more abstract specification's behaviours, layered so low-level code refines a high-level model.
- Constant-time verification
- Proving that a program's control flow and memory access pattern do not depend on secret data, so timing and cache side channels cannot leak keys.
- Arithmetization (R1CS, PLONKish, AIR)
- The encoding of a computation as polynomial constraints over a finite field: rank-1 constraint systems (Groth16, gnark), PLONKish gates with copy and lookup constraints (Halo2), or algebraic intermediate representations over execution traces (STARKs, Plonky3, SP1).
- Extraction (code to model)
- The step that turns a deployed circuit or program into the object a prover reasons about, whether by instrumenting synthesis (Halva), compiling to an IR (LLZK), or translating source (hax, Aeneas).
- Witness generation vs constraints
- Witness 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.