# Why is Proof Checker required in Proof Carrying Code

In the classical PLDI'98 paper by Necula, "The design and implementation of a certifying compiler", the high-level verifier uses:

1. VCGen to generate verification conditions (safety predicates)
2. First-order logic theorem prover to prove the conditions
3. LF proof checker to check the proof from step (2)

I am a bit confused by step (3). Why is it required at all? Will just (1) and (2) not suffice? Why don't we just trust the proof generated by a theorem prover?

## 1 Answer

The purpose of the proof checker is to minimise the trusted computing base.

By having a proof checker, neither the compiler nor the theorem prover need to be correct. The paper makes this point on Page 3:

Neither the compiler nor the prover need to be correct in order to be guaranteed to
detect incorrect compiler output. This is a significant advantage since the VCGen and
the  proof checker are significantly simpler than the compiler and the prover.


A proof checker is just a couple of lines of code, and can be hand-inspected for correctness. In contrast, an automated prover that performs well is extremely complex and unlikely to be correct, although with well-tested and widely used provers, the mistakes will be in edge cases that might not be easy to trigger. Have a look at the 30k LOC C code that make up Lingeling, a state-of-the-art SAT solver to see just how complicated automated theorem provers can be. Without a proof checker, you'd have to prove correct that theorem prover. This is beyond whaty we can economically do in 2015.

• I am surprised that proofs constructed by ATPs can be buggy. (I thought ATP's can be incomplete but not unsound/buggy) I am less informed here. I'll be happy to know if there are any known instances of expensive mistakes in proofs generated by ATPs. – Ram Aug 31 '15 at 19:42
• @Ram There are thousands of tiny soundness bugs in the history of any serious automatic theorem prover. See e.g. stackoverflow.com/questions/12281085/… or the revision history of any such tool on github. – cody Aug 31 '15 at 21:19
• @Ram In addition to Cody's great advice, I recommend to learn from experience: write a little ATP such as a basic SAT solver. That can be done in a few lines of code. Then try and make it perform well by adding e.g. clause learning, watched literals or interesting variable selection heuristics. Then think about the experience ... – Martin Berger Sep 1 '15 at 13:35