Reasoning foundations
Trusted computing base
Abbreviated TCB
The code and assumptions that must be correct for a result to be valid.
Definition
Trusted computing base
The trusted computing base (TCB) contains every part whose failure could make an invalid result appear valid.
A small checker can reduce the amount of code that must be trusted, but the language semantics and the formalized statement also remain part of the claim.
01
Example
For a kernel-checked theorem, the kernel and its primitive rules belong to the TCB. A tactic that only creates a proof term need not belong to it.
02
Important distinction
Small code is easier to inspect, but size alone does not establish correctness.
After reading this article, you should be able to
- Define TCB in the sense used on this site.
- List the trusted parts of a simple solver or proof-checking route.