This repository is the homepage of the course Formal Verification. It contains essential materials and links about course organization and learning.
- Professor: Viktor Kunčak
- PhD Teaching Assistant: Lazar Milikic
- Student Assistant: Jacopo Moretti
The grade is based primarily on computer-based and paper-based exams done in class during the semester. A smaller part of the grade is based on a project done in groups and presented at the end of the semester.
Passing the course requires being present in several examinations throughout the semester.
| Percentage | Work Description | Group/Individual | Submission | Date/Deadline |
|---|---|---|---|---|
| 5% | first lab (using Stainless) | group | Moodle | 2 October 20:00 |
| 5% | second lab (using Lean) | alone | Moodle | 27 October 20:00 |
| 30% | in-class exam solving problems in Lean on computers | alone | live | 29 October 15:00-19:00 |
| 40% | in-class paper written exam | alone | live | November |
| 20% | final group projects and their presentations in class | group | live | last weeks of the semester |
The use of LLMs is allowed for final group projects, but you need to document how you use them. You are also welcome to use search and AI tools to clarify your understanding of the material outside of the exams. Aside from commercial providers, note that you can use EPFL-hosted open-weight models available at https://chat.rcp.epfl.ch/ from within EPFL network.
In this course, we introduce formal verification as a principled approach for developing systems that do what they are expected to. One of the primary vehicles we use is Lean language for programming and proving that comes with a large mathematics library and was also used to formalize, e.g., Sphere packing results, the proof of Fermat's last theorem as well as the Finite time blowup for Navier–Stokes and Euler equations.
The course has two aspects:
- learning the practice of formal verification - how to use tools (Stainless, Lean) to construct verified software
- understanding the principles behind formal verification and the ways in which verification tools work
We will have the following types of activities:
- Lecture hours where we introduce the material or hear a guest lecture
- Exercise hours, which we hand out and do not grade, and that help you prepare for the in-class paper exam
- Lab hours, where you work to solve the graded labs and ask questions, prepare for the in-class computer exam, and work on your final project
- Final project presentations
To see the material, please visit https://mediaspace.epfl.ch , log in with your EPFL credentials and select this channel. Slides and listings are attached underneath the videos.
| Week | Day | Date | Labs Active | Time | Room | Topic | Videos & Slides |
|---|---|---|---|---|---|---|---|
| 1 | Thu | 10.09.2026 | ..... | 15:15 | ELA2 | Lecture 1 (PDF: A, B) (playlist) | Intro to FV, Intro to Stainless, Auxiliary Assertions, Unfolding, Disasters, Successes, and Inductive Invariants |
| ..... | 17:15 | ELA2 | Lecture 2 (PDF) (playlist) | Dispenser Example, Finite Systems Expressed with Formulas | |||
| Reading: | HandMC-Ch.10 | ||||||
| Follow: | Stainless Tutorial Videos and materials | ||||||
| Fri | 11.09.2026 | ..... | 13:15 | INR219 | [Lecture 3] (PDF: A, B) (playlist) | What is a Formal Proof? and Propositional Resolution | |
| 2 | Thu | 17.09.2026 | 1.... | 15:15 | ELA2 | Lab 1 | Stainless |
| 1.... | 17:15 | ELA2 | Lab 1 | Stainless | |||
| Fri | 18.09.2026 | 1.... | 13:15 | INR219 | Exercises 1 | Propositional logic, Transition Systems | |
| 3 | Thu | 24.09.2026 | 1.... | 15:15 | ELA2 | finish Lecture 3 | Propositional Resolution |
| 1.... | 16:15 | BC420 | Guest Lecture | IC Colloquium: Abstract Interpretation on irregular programming environments. Background: Abstract Interpretation in a Nutshell | |||
| 1.... | 17:15 | ELA2 | Lab 1 | Stainless | |||
| Fri | 25.09.2026 | 1.... | 13:15 | INR219 | Lecture 4 | Automating First-Order Logic Proofs Using Resolution | |
| 4 | Thu | 01.10.2026 | 1.... | 15:15 | ELA2 | Lecture 5 | Lean introduction |
| 1.... | 17:15 | ELA2 | Lab 1 | Stainless | |||
| Fri | 02.09.2026 | 1.... | 13:15 | INR219 | Lecture 6 | Propositions as Types. Syntax and Semantics of Propositional Logic in Lean |
- Lean documentation: https://lean-lang.org/learn/
- Scala documentation (for first lab, optionally project): https://docs.scala-lang.org/
- [CalComp] The Calculus of Computation - Decision Procedures with Applications to Verification, 2007, from Springer, from EPFL library, by Aaron Bradley and Zohar Manna.
- [HandMC] Handbook of Model Checking, 2018, from from Springer, from EPFL Library, edited by Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, Roderick Bloem.
- [HandAR] Handbook of Practical Logic and Automated Reasoning, 2009, from Cambridge University Press and from EPFL Library, by John Harrison