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:


VCGen to generate verification conditions (safety predicates)
First-order logic theorem prover to prove the conditions
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?
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.