deep-roots learning program · module 21
Module 21 — Formal verification
Every chapter: first principles, What insiders know, a See it yourself lab, connections, and a quiz with worked answers.
01
What is a proof of a program
Specs, soundness, the LCF kernel — why the checking machine can be 100× smaller than the proving machine.
→
02
Model checking and the state explosion
Brute-force proof over states, BDDs and SAT as compressed truth tables, BMC, the memory budget as the frontier.
→
03
The verified kernel
seL4: the proof effort in person-years, the 100:1 proof-to-code ratio, what the theorem says and doesn't.
→
04
The borrow checker is separation logic
Ownership as a decidable fragment; the lineage from Reynolds/O'Hearn to NLL; Miri as the operational checker.
→
05
Verified compilers and crypto
CompCert's correctness theorem, the verified-field-arithmetic stacks, and the honest boundary of proof.
→
the exam