<p>The purpose of the proof checker is to minimise the <a href="https://en.wikipedia.org/wiki/Trusted_computing_base">trusted computing base</a>. </p>

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

<pre><code>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.
</code></pre>

<p>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 <a href="http://fmv.jku.at/lingeling/">Lingeling</a>, 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.</p>

CC BY-SA 3.0
2015-08-31T19:42:12.640Z
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
CC BY-SA 3.0
2015-08-31T21:19:25.697Z
@Ram There are thousands of tiny soundness bugs in the history of any serious automatic theorem prover. See e.g. http://stackoverflow.com/questions/12281085/bug-changing-order-of-assertions-affects-satisfiability or the revision history of any such tool on github.
cody
CC BY-SA 3.0
2015-09-01T13:35:35.367Z
@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
CC BY-SA 3.0
2015-08-30T16:51:46.037Z
2015-08-30T17:17:27.907Z
2015-08-30T17:17:27.907Z
Martin Berger
<p>In the classical PLDI'98 paper by Necula, "The design and implementation of a certifying compiler", the high-level verifier uses:</p>

<ol>
<li>VCGen to generate verification conditions (safety predicates)</li>
<li>First-order logic theorem prover to prove the conditions</li>
<li>LF proof checker to check the proof from step (2)</li>
</ol>

<p>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? </p>

<proof-theory><automated-theorem-proving><program-verification>
Why is Proof Checker required in Proof Carrying Code
Ram
# Why is Proof Checker required in Proof Carrying Code

(Asked by: username_0 on 2015-08-30)

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?

**Tags:** proof-theory, automated-theorem-proving, program-verification

---

## 1 answers

### Answer by username_1 on 2015-08-30. Score: 19 | Accepted 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.

> **Comments:**
> **username_0**: 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.  
> **username_2**: @Ram There are thousands of tiny soundness bugs in the history of any serious automatic theorem prover. See e.g. http://stackoverflow.com/questions/12281085/bug-changing-order-of-assertions-affects-satisfiability or the revision history of any such tool on github.  
> **username_1**: @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 ...  

---

