A framework for certified software Specifications ↓ No Proof Proof Checker Machine Yes code CPU certified code (code proof) ·specifications: lang.semantics+program safety/security/correctness... automated proof checker need not trust the correctness of proofs A framework for certified software • certified code (code + proof) • specifications: lang. semantics + program safety/security/correctness … • automated proof checker need not trust the correctness of proofs Proof Checker Yes CPU Specifications Proof Machine code No