Must be in the Computer Science Master's or Doctoral program; or permission of the instructor.

This course explores the design and implementation of mechanically verif ied systems software, including operating systems, compilers, and virtua l machines. The course combines foundations from program verification, t heorem proving, and systems programming with emerging AI-assisted workfl ows that pair proof assistants with coding assistants. Students will stu dy representative verified systems, evaluate current tools, and gain han ds-on experience specifying, implementing, and proving correctness prope rties of systems code.