Formal Methods for AI
2026
MSc Computer Science · Leiden University
General information
Formal Methods for AI is a master-level course on automated reasoning, model checking, certification, neural control, and runtime monitoring for AI-enabled systems.
- Course goal: The goal of the course is to carry out a research-oriented project in formal methods for AI: re-run a state-of-the-art FM&AI paper and possibly 1) study it in a new application and/or 2) investigate your own novel extension. A successful project may form the basis of a workshop paper or a future master’s thesis.
- Course code: 4343FMFAIY
- Instructor: dr. Emily Yu
- Dates: 2 September–2 December 2026, every Wednesday
- Format: lectures, paper presentations, discussions, homework, and project work
Course schedule
All course materials are available on Brightspace.
When
Class
Reading / presentation
Deliverable
Wed 2 SeptemberWeek 1
Introduction to formal methods for AI
Review the paper list and project-list PDF on Brightspace.
Review the project options on Brightspace and form a group of two or three students.
Wed 9 SeptemberWeek 2
Model checking
Foundational reading; no presentation
Due Wed 9 Sep Project partners and top two project choices.
Wed 16 SeptemberWeek 3
Certification
Foundational reading; no presentation
Due 16 Sep Project proposal: 2–3 pages, 10pt font, single-spaced, single column. Homework 1 Released.
Wed 23 SeptemberWeek 4
Neural control
—
Homework 1 Due before class.
Wed 30 SeptemberWeek 5
Monitoring
—
Homework 2 Released.
Wed 7 OctoberWeek 6
Guest lecture: SAT solving
No student paper presentation
Homework 2 Due before class. Project work Bring a working implementation or encoding for feedback.
Wed 14 OctoberWeek 7
Paper presentations
- Grigory Neustroev, Mirco Giacobbe, and Anna Lukina. “Neural Continuous-Time Supermartingale Certificates.” AAAI 2025, pp. 27538–27546.
- Thom Badings, Wietze Koops, Sebastian Junges, and Nils Jansen. “Policy Verification in Stochastic Dynamical Systems Using Logarithmic Neural Certificates.” CAV 2025, pp. 349–375.
Progress update
Wed 21 OctoberWeek 8
Midterm project presentations
Project progress presentations and feedback
Due Wed 21 Oct Midterm review: 3 slides maximum.
Wed 28 OctoberWeek 9
Paper presentations
- Fabian Kresse, Emily Yu, Christoph H. Lampert, and Thomas A. Henzinger. “Logic Gate Neural Networks Are Good for Verification.” NeuS 2025, pp. 90–103.
- Anagha Athavale, Ezio Bartocci, Maria Christakis, Matteo Maffei, Dejan Ničković, and Georg Weissenbacher. “Verifying Global Two-Safety Properties in Neural Networks with Confidence.” CAV 2024, pp. 329–351.
Project implementation and experiments
Wed 4 NovemberWeek 10
Paper presentations
- Luan Viet Nguyen, James Kapinski, Xiaoqing Jin, Jyotirmoy V. Deshmukh, and Taylor T. Johnson. “Hyperproperties of Real-Valued Signals.” MEMOCODE 2017, pp. 104–113.
- Tzu-Han Hsu, Arshia Rafieioskouei, and Borzoo Bonakdarpour. “HypRL: Reinforcement Learning of Control Policies for Hyperproperties.” NeurIPS 2025.
- Benedikt Maderbacher, Stefan Schupp, Ezio Bartocci, Roderick Bloem, Dejan Ničković, and Bettina Könighofer. “An Adaptive, Provable Correct Simplex Architecture.” International Journal on Software Tools for Technology Transfer, 2025.
Project implementation and experiments
Wed 11 NovemberWeek 11
Paper presentations
- Dawei Sun, Susmit Jha, and Chuchu Fan. “Learning Certified Control Using Contraction Metric.” CoRL 2020, pp. 1519–1539.
- Sterre Lutz, Matthijs T. J. Spaan, and Anna Lukina. “VeRecycle: Reclaiming Guarantees from Probabilistic Certificates for Stochastic Dynamical Systems after Change.” IJCAI 2025, pp. 457–465.
- Kevin Batz, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Philipp Schröer. “PrIC3: Property Directed Reachability for MDPs.” CAV 2020, pp. 512–538.
Project implementation and experiments
Wed 18 NovemberWeek 12
Paper presentations
- Mirco Giacobbe, Daniel Kroening, Abhinandan Pal, and Michael Tautschnig. “Neural Model Checking.” NeurIPS 2024, pp. 86375–86398.
- Thomas A. Henzinger, Kaushik Mallik, Pouya Sadeghi, and Đorđe Žikelić. “Supermartingale Certificates for Quantitative Omega-Regular Verification and Control.” CAV 2025, pp. 29–55.
Project implementation and experiments
Wed 25 NovemberWeek 13
Paper presentations
- Andrei Aleksandrov, Malte Jackisch, and Kim Völlinger. “The Rocq-NN-Roll Prover: Soundly Verifying Hyperproperties of Neural Networks in Rocq.” CAV 2026, pp. 480–503.
- Omri Isac, Idan Refaeli, Haoze Wu, Clark Barrett, and Guy Katz. “PICID: Proof-Driven Clause Learning in Neural Network Verification.” FMCAD 2026.
Due Sun 29 Nov Final report: 5–6 pages, 10pt font, single-spaced, two-column.
Wed 2 DecemberWeek 14
Paper presentations and final project presentations
Final assigned paper presentations
Due 2 Dec Final presentation: 10-minute talk. Due Fri 4 Dec Artifact submission.
Paper Presentations
Students assigned to a paper will present the work and lead the class discussion. Unless announced otherwise, plan for approximately 10 minutes of presentation followed by discussion. Paper-presentation sessions will also leave time for students to ask project-related questions. The presentation template is available on Brightspace. The presentation should be concise, self-contained, and address:
- Motivation and novelty: What problem does the paper address, why does it matter, and what is new?
- Key insights and contributions: What ideas and technical results enable the approach?
- Formal-methods approach: Which formal technique is used, and how are the system and properties formalized?
- Tool and evaluation: What are the tool inputs and outputs, how is the approach evaluated, and what are the main results?
- Critical assessment: What are the strengths, limitations, and possible improvements?
- Discussion questions: Compile a list of questions to start the class discussion on the paper. Questions may address aspects you wish the paper had handled better, the paper’s broader implications, or ways you would extend the work—for example, by changing the problem or solution or by using a different formal-methods approach.
Project
You will carry out a course-long research project in a group of two or three students. You may choose a topic from the project-list PDF on Brightspace or propose a closely related idea, subject to approval. The project deliverables are:
- Project partners and preferences: 9 September 2026. Submit the names of all group members and your top two project choices.
- Project proposal: 16 September 2026. 2–3 pages, 10pt font, single-spaced, single column.
- Midterm review: 21 October 2026. 3 slides maximum.
- Final report: 29 November 2026. 5–6 pages, 10pt font, single-spaced, two-column. Use the FM for AI report template on Overleaf.
- Final presentation: 2 December 2026. 10-minute talk.
- Artifact submission: 4 December 2026.
Assessment
Final grade components
To pass the course, each component grade must be at least 5.5 and students must attend at least 80% of lectures.