FVLearn Formal Verification

Courses

Level 1

Formal Verification Foundations

Learn to say exactly what code must do, then check it with a verifier.

This course teaches one habit: before you trust code, say exactly what it must always do, then have a tool check it. You are not training to become a proof specialist. A green check covers only the claims you wrote.

How each exercise works

  1. Read the short brief.
  2. Edit the code in the browser. It is often a single line.
  3. Hit Verify. A real verifier decides pass or fail, not an AI.
  4. Stuck? Reveal the hints one at a time. The last hint gives the answer.

Exercises open in order. The “Meet” pages are always open, so you can try a finished example first.

What you will learn

Each word below is a question you learn to ask about code.

  • Specification — what exactly are we claiming?
  • Precondition — what can the code assume when it starts?
  • Postcondition — what must be true when it finishes?
  • Counterexample — which concrete case breaks the claim?
  • Invariant — what stays true while something changes?
  • Termination — does the loop ever stop?
  • State machine — what states can the system be in, and which steps move it between them?
  • Model checking — did the tool look at every state this small model can reach?
  • Safety — what must never happen?
  • Liveness — what must eventually happen?
  • Proof — which steps show the claim holds?

How the units fit together

Unit 0 is a short orientation. Units 1–5 check one function with Dafny. Units 6–9 check a design with TLA+ and its checker, TLC. Unit 10 is a short look at Lean, for the rare step a checker cannot finish. Unit 3 teaches you to read a failed check, and Unit 4 asks what stays true through a loop. Unit 5 adds whether the loop ever stops. Unit 8 asks the safety question when steps can happen in any order.

0 of 11 units done · 0 of 24 exercises verified

The three tools

Each unit uses one of these. Open an intro to run a finished example before you start.

  1. 00Orientation

    Start here. Run a finished example, and see what Verify does and what a green result does and does not tell you.

  2. 01Specifications

    What exactly are we claiming? A specification is the full claim about what code does. A postcondition is the part that says what is true of the result. A claim that says too little still goes green.

  3. 02Preconditions & postconditions

    What can the code assume when it starts, and what must it guarantee when it finishes? Dafny also checks every division and array index, written or not.

    • Prevent an overdraftState what callers must provide so the balance can never go negative.locked
    • A check you did not writeNotice that Dafny also checks that every operation in the body is allowed, and supply the precondition that makes this one safe.locked

  4. 03Counterexamples

    You have already seen red results. Now read one on purpose: the tool shows one input that breaks the claim. Trace it like a failing test.

    • Debug with a counterexampleRead the concrete input that breaks a correct claim, then fix the code.locked
    • Follow the branchUse the counterexample's inputs to work out which branch ran, then fix that branch.locked

  5. 04Invariants

    What stays true on every pass through a loop, so it is still true when the loop ends?

    • The loop forgetsSay what stays true on every pass through the loop, so it is still true when the loop stops.locked
    • A loop that addsSay what the running total is part-way through, on every pass.locked

  6. 05Loop verification

    Does the loop ever stop? Then the invariant question again, over many positions of an array.

    • Does it stop?Name a quantity that shrinks on every pass and cannot go below zero, so the loop must stop.locked
    • The greatest elementSay what is true of the part already scanned: the value is in it, and nothing in it is larger.locked
    • An index that cannot go out of rangeSay what stays true of the search window, so the search never looks off the end and never misses the key.locked

  7. 06State machines

    A design is a set of states and the steps between them. Describe one, then name what must hold in every state.

  8. 07Model checking

    Did the checker look at every state this small model can reach? When it finds a bad one, it shows the steps that led there.

    • Read a traceRead the steps the checker found that lead to a bad state. Do not repair it yet.locked
    • Guard the actionChange the withdrawal step so a negative balance can never be reached. Leave the safety property alone.locked

  9. 08Concurrency

    The same safety question, when steps from different parts can happen in any order. What must never be true?

    • Two leadersSee an order of steps that ends with two leaders at once.locked
    • At most oneChange the step so two leaders cannot happen. Leave the property as “at most one leader.”locked

  10. 09Safety & liveness

    Safety: what must never happen? Liveness: what must eventually happen?

    • Eventually a leaderSee a run that is safe, yet never elects anyone.locked
    • FairnessState the assumption that makes “eventually a leader” true.locked

  11. 10Introduction to proof

    When a checker cannot finish, which steps show the claim holds? A narrow skill you will rarely need, not the point of the course.