Easier to read with cream paper, a tint, more contrast or larger text? Choose your colours and text, once, for every page.

Free module

Formal methods

Learn formal methods hands on: prove claims with Z3, find races and check locks with SPIN, model with TLA+ and Alloy.

6 lessons340 min lessonCore computer science

The lessons

Each lesson is free to read in full. Create a free account to run its commands in a live lab and to sit its quizzes and tasks.

  1. 1 · Virtual machine lab

    Why testing cannot prove a program correct

    I can say what a test shows and what a proof shows.

    Read the lesson

  2. 2 · Virtual machine lab

    Proving a claim with the Z3 solver

    I can ask Z3 whether a claim always holds.

    Read the lesson

  3. 3 · Virtual machine lab

    Finding a race condition with SPIN

    I can find a race between two processes in a trace.

    Read the lesson

  4. 4 · Virtual machine lab

    Writing a lock and checking mutual exclusion

    I can write a lock and have SPIN report no errors.

    Read the lesson

  5. 5 · Virtual machine lab

    Invariants and counterexamples in TLA+

    I can write an invariant and read the counterexample for a broken design.

    Read the lesson

  6. 6 · Virtual machine lab

    Checking a model with Alloy

    I can read the counterexample Alloy gives for a claim about a model.

    Read the lesson

Worked in a real lab

Every lesson of this module is worked in a lab started for you alone. The labs it uses:

Teaching a class? Set this module for your students with a teacher guide, marked assignments and a lab for every student.