This graduate-level course studies how formal reasoning techniques are used to design, analyze, and secure modern software systems operating in open, adversarial, and intelligent environments. Rather than focusing solely on individual verification tools, the course presents reasoning as a system-level activity that combines automated solvers, human-guided proofs, and AI-based agents. Foundational constraint-solving techniques provide the substrate, while higher-level reasoning pipelines are applied to complex settings such as AI-assisted programming and blockchain protocols, where correctness, security, and incentives interact. Through case studies and projects, students learn how to build reasoning systems that scale beyond fully automated verification and provide strong correctness guarantees in practice.
Once the quarter starts, instructor approval is required to maintain enrollment in the course, including if students do not have the listed pre-requisite courses completed.