sorryfreeLast reviewed 2026-09-13
Index › Glossary › Trusted computing base and verification boundary

Trusted computing base and verification boundary

Direct answerEverything 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.

In more detail

A responsible verification deliverable lists its TCB explicitly: which Lean axioms, whether native_decide was used, how constraints were extracted from the codebase, and what surrounding code is unverified. zk.golf enforces an axiom allowlist for exactly this reason. Ask every vendor for the boundary in writing.

Circuit soundness, Circuit completeness, Underconstrained circuit, Overconstrained circuit, Symbolic vs computational model, Specification gap, 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