Verification = TCB/PB Reduction

Said differently, we verify the theorem, and the proof represents the verification process. The proof author can choose an abstraction level for the axioms and the proof rules, to trade-off between proof simplicity and the level of rigour. Incorrect Proof Rules: If any of the proof rules is unsound, then the proof steps can become unsound, which in turn results in an incorrect proof. The value of a formal verification effort is that it reduces your Trusted Computing Base/Probability of a Bug, or TCB/PB. In our strlen example, if the implementation has been formally verified, then we know that for there to be a bug in the implementation, there must be a bug either in the specification or there must be a bug in the logical encoding of the C programming language semantics or there must be a bug in the proof rules or there must be a bug in the proof checker. For some components of the proof, such as the specification, it makes sense to quantify the TCB reduction through SLOC. But for other components, such as axioms, proof rules, and proof checkers, we are not relying on SLOC reduction but on the fact that these are infrastructural components that have been heavily tested and are often in heavy production use. Further, even if any of these infrastructural verification components have a corner-case bug, it is very unlikely that the bug manifests itself in a way that it causes an incorrect proof to go through. At worst, a corner-case bug in the verification tools would cause the verification process to end abruptly, not cause a wrong proof to go through.