What is Trusted computing base and verification boundary? Definition and why it matters
================================================================================

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.

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.

Source page: https://sorryfree.com/glossary/trusted-computing-base/
Compiled by: sorryfree editors (https://sorryfree.com/about/)
Last reviewed: 2026-09-13