Language models now produce code and mathematical proofs in quantity, but they offer no guarantee that what they produce is correct, and reviewing it by inspection does not scale. Formal verification provides such a guarantee: a specification states precisely what a program or a theorem must satisfy, and a proof that it does so can be checked mechanically by a small program, independently of how that proof was found. This course develops that idea from its foundations to its practical use. The theory begins with the untyped λ-calculus and builds through the λ-cube to the type theory on which Lean 4 rests, including the correspondence between propositions and types that makes proof checking a form of type checking. The practice begins with Lean as a programming language and ends with programs that carry contracts and machine-checked proofs of their specifications. On completing the course, students will be able to write formal specifications, prove that implementations satisfy them, and determine what an AI-generated program or proof does and does not guarantee.
lecture
lecture
No class
lecture
lecture
lecture
lecture
lecture
lecture
lecture
lecture
lecture
lecture