A Trustworthy Proof Checker

Andrew W. Appel, Neophytos Michael, Aaron Stump, Roberto Virga

Research output: Contribution to journalArticlepeer-review

21 Scopus citations


Proof-carrying code (PCC) and other applications in computer security require machine-checkable proofs of properties of machine-language programs. The main advantage of the PCC approach is that the amount of code that must be explicitly trusted is very small: it consists of the logic in which predicates and proofs are expressed, the safety predicate, and the proof checker. We have built a minimal proof checker, and we explain its design principles and the representation issues of the logic, safety predicate, and safety proofs. We show that the trusted computing base (TCB) in such a system can indeed be very small. In our current system the TCB is less than 2,700 lines of code (an order of magnitude smaller even than other PCC systems), which adds to our confidence of its correctness.

Original languageEnglish (US)
Pages (from-to)231-260
Number of pages30
JournalJournal of Automated Reasoning
Issue number3-4
StatePublished - 2003

All Science Journal Classification (ASJC) codes

  • Software
  • Computational Theory and Mathematics
  • Artificial Intelligence


  • Proof checker
  • Proof-carrying code


Dive into the research topics of 'A Trustworthy Proof Checker'. Together they form a unique fingerprint.

Cite this