CMSC 818C: Verified Systems Programming with Proof Agents

Instructor: David Van Horn.

Spring 2027

Class meetings: Tuesdays and Thursdays, 2–3:15 p.m., IRB 2207.

This course explores the design and implementation of mechanically verified systems software, including operating systems, compilers, and virtual machines. The course combines foundations from program verification, theorem proving, and systems programming with emerging AI-assisted workflows that pair proof assistants with coding assistants. Students will study representative verified systems, evaluate current tools, and gain hands-on experience specifying, implementing, and proving correctness properties of systems code.

This site collects course notes and supporting material as they develop. Browse the notes, work through the projects, or read about the course.