Course path
Choose a course
These courses teach you to say exactly what code must do, then check it with a tool. That includes code you did not write, such as code an AI generated. Each course is a series of short exercises, and each exercise opens after you finish the one before it.
New to this? Take Level 1 first. It is free. Levels 2 to 5 are part of Learn Formal Verification Pro.
Level 1
Free
Formal Verification Foundations
Learn to say exactly what code must do, then check it with a verifier.
Start here if you are new. You do not need to know Dafny, TLA+, Lean, or any proofs. Tools: Dafny, TLA+, Lean
0 of 11 units done · 0 of 24 exercises verified
Start course →
Level 2
Pro
Program Verification with Dafny
Verify real properties of ordinary code, including code you did not write. When Dafny stops, work out which claim it could not prove and supply what is missing. A green check covers only the claims that were written.
Best after Level 1, but not required. You work on longer programs and learn what to do when Dafny stops. Tool: Dafny
0 of 7 units done · 0 of 48 exercises verified · capstone not finished
See the syllabus →
Level 3
Pro
Specification Engineering
A green check says the code meets the specification, not that the specification says what you needed. Find what is missing, strengthen it, and stop it from asking for too much.
Best after Level 2, but not required. Every proof passes, and you find what the specification fails to say. Tools: Dafny, TLA+
0 of 7 units done · 0 of 33 exercises verified · capstone not finished
See the syllabus →
Level 4
Pro
AI-Assisted Verification
Use an AI assistant without trusting it blindly. You own the requirements and the specification. The assistant writes code and proof annotations. The verifier checks one against the other, and you audit what it cannot.
Best after Level 3, but not required. You work with an AI assistant and learn what the verifier does and does not tell you about its work. Tools: Dafny, TLA+
0 of 5 units done · 0 of 27 exercises verified · capstone not finished
See the syllabus →
Level 5
Pro
Verification of Real Systems
Verify realistic software with the training wheels off. Each project hands you a system and its requirements, then someone else's verified code, and finally a system and a brief: you decide what it must do.
Best after Level 4, but not required. You choose from nine projects, from a login service to a consensus protocol. Every project is open from the start, and its three stages open in order. Tools: Dafny, TLA+
0 of 9 projects done · 0 of 27 stages verified
See the syllabus →