University of Waterloo · Electrical and Computer Engineering · Winter 2027

Automated Verification

Building Reliable Software in the Age of AI

ECE 750 T29 · Graduate course · Instructor Arie Gurfinkel

AI is accelerating software development, and it is just as good at finding and exploiting the weaknesses of existing systems. This course is about establishing that software behaves as intended: formulating correctness claims, checking them with automated verification tools, and judging what a successful check actually guarantees. We move from practical verification tasks to the reasoning behind the tools (verification conditions, SMT solving, memory and ownership, and automatic invariant discovery) and on to proof assistants, where AI agents help build specifications and proofs that students learn to guide and review. Examples come from software libraries, systems code, and compiler transformations. Details are in the syllabus.

Weekly schedule

Lectures, slides, and readings →

01What does it mean to verify?Correctness claims, specifications, assumptions, vacuity, and bounded checking.Lectures 1–2 02Deductive verificationContracts and inductive invariants for Rust; AI-assisted proof development.Lectures 3–4 03SMT and equality reasoningSolver interfaces, models, cooperating decision procedures, congruence closure.Lectures 5–6 04Verification conditionsReducing program correctness to logic; transformations and query encodings.Lectures 7–8 05Memory and ownershipAliasing, array-based memory models, ownership, and prophecy.Lectures 9–10 06Automatic invariant discoveryAbstract interpretation for low-level code such as kernel extensions.Lectures 11–12 07Horn clauses and inductionConstrained Horn clauses; from bounded checks to inductive proofs.Lectures 13–14 08Property-directed reasoningIC3/PDR, generalization, summaries, and the effect of encodings.Lectures 15–16 09Proof assistants with AI agentsReading formal models and theorems; reviewing agent-assisted proofs in Lean.Lectures 17–18 10From Rust to functional proofsFunctional translation, embeddings, and reasoning about mutation.Lectures 19–20 11Checking verification toolsProduct programs, translation validation, and AI-assisted verifier development.Lectures 21–22 12Student investigationsProject presentations and synthesis of the course's methods and limits.Presentations