From CakeML to Proof Checking, and Back Again
summary
CakeML now comprises about 750,000 lines of code (over a million including auxiliaries) and delivers a formally verified compiler from a high‑level ML-like source down to machine bytes, including a verified bootstrap compiler that compiles itself, five ISA targets with an ARMv8 authoritative semantics, runtime eval that installs compiled bytes, and end‑to‑end verified proof checkers for SAT and related tools that stream proofs (Katico integration) and are used in competitions (verified checking is effectively free).
AI-written summary · about
chapters (17)
- 0:00Introduction
- 1:05CakeML overview
- 3:12Compiler architecture
- 10:02Verified bootstrapping
- 13:32Binary extraction
- 14:15Verification tools
- 17:07New front ends
- 19:57Verified targets
- 21:22Dynamic evaluation
- 25:06Trustworthy reasoning
- 28:37Certifying algorithms
- 30:22CakeML in SAT
- 32:26AI solvers
- 33:53Live demo
- 35:19Symbiotic relationship
- 37:05Summary
- 37:45Q&A
related talks
01h 05mMuch Still to Do in Compiler Verification (A Perspective from the CakeML Project)
24mCakes That Bake Cakes: Dynamic Computation in CakeML
15mThey're the same picture: a software-verification flow adapted for hardware verification
17mPureCake: A Verified Compiler for a Lazy Functional Language
21mVerified VCG and Verified Compiler for Dafny
18mBaking for Dafny: A CakeML Backend for Dafny
15mDo You Have Space for Dessert? A Verified Space Cost Semantics for CakeML Programs
16mTowards formally secure compilation of verified F* programs against unverified ML(…)