Proof checkers for proof-carrying code (and similar systems) can suffer
from two problems: huge proof witnesses and untrustworthy proof rules.
No previous design has addressed both of these problems simultaneously.
We show the theory, design, and implementation of a proof-checker
that permits small proof witnesses and machine-checkable proofs
of the soundness of the system.