Formal methods lab: Z3, SPIN, TLA+ and Alloy on one VM

This lab gives each student four verification tools in one Ubuntu VM. Testing shows that a design works on the cases tried. A formal method asks a machine to look at every case and either prove the property or return a counterexample. Students use Z3, a solver, SPIN, a model checker for Promela, TLA+ with its checker TLC, and Alloy, each on one small problem.

Nothing is installed on the student’s computer. The tools are the real ones, and the lab’s README gives the problems and none of the answers.

What students learn

What it means to check a design instead of trying it, in four parts. With Z3 they state the rules of an exam timetable and then a claim the rules make true, which Z3 proves by finding that its opposite has no solution. With SPIN they find a race between two processes in a trace, then write a lock so that no error is left. With TLA+ they write the invariant that says what a lock is for, read the counterexample TLC prints for a lock that does not lock, and fix it. With Alloy they read a counterexample drawn as people and friendships, and repair the model with a new fact.

Run it in your browser

VM labs are set as a lab task in a module, and the sample is on the lab’s page. The machine is small: one CPU, 1 GB of memory and 10 GB of disk. Each Java tool is limited to 128 MB and the whole lab fits comfortably. Z3 and SPIN need only Ubuntu’s archive. TLA+ and Alloy are downloaded from GitHub, which a guest VM with no account cannot reach, so those two parts need a signed-in VM.

  1. Add the lab. In a module you teach, add a task and choose the Ubuntu VM lab card. The page shows a short description of the machine instead of a compose file.
  2. Start from the sample. The page offers ready-made labs to start from. Choose Formal methods. Using a sample replaces the text, and Undo brings yours back.
  3. Publish and start your own copy. Publish, then Start. The lab’s own setup script installs Z3, SPIN and a Java runtime from Ubuntu’s archive, downloads TLA+ and Alloy from their GitHub releases and checks each file against a fixed checksum, the first time the VM starts, in a few minutes.
  4. Open the terminal. Open its terminal and read README.md in the home folder: it says what to do in four parts and gives none of the answers.

A basic lesson on this lab

Formal Methods Basics is a small lesson worked in this lab, which is an Ubuntu VM. It has a hook, an I can outcome, key words, a starter, a check after each idea, a common mistake and an exit check, and each step has a Run button that types its command into the machine’s terminal. A student asks Z3 a question it can answer and one it cannot, lets SPIN find the race in the lab’s own model and replays it, reads the counterexample TLC prints for an invariant that is false of a correct lock, and sees an Alloy instance.

The lesson looks around and leaves the lab’s own tasks to the student, so it hands out no answers.

How it is marked

The lab has a check, and it believes the tools and never the student’s own words. Z3 itself compares the student’s timetable rules with the README’s, so a hand-written answer or a missing rule fails, and the claim must follow from the rules and not be true without them. SPIN runs the student’s lock inside a harness of the check’s own and the lock may name nothing the harness owns. TLC runs the fixed lock with the check’s own invariant as well as the student’s, both processes must be able to enter, and the student’s invariant must be broken by the shipped broken lock, so an invariant of TRUE fails. Alloy opens the student’s model from a file of its own with its own assertions, which must hold, and a run that must still find a group of friends. The first line of what the check printed says why.

  1. Hand it out. Assign the lab like any task, with a due date if you want one. Each student gets a VM of their own, kept between sessions if they have an account.
  2. Run the check. On a student’s row in the class list, press Run the check. It starts a copy of their saved machine that is not saved back, runs the lab’s check script as root and shows whether it passed, what it printed and when. The student is not told the result.
  3. Mark it. Read the first line of what the check printed: it names the part and says what is not right, such as a rule Z3 finds missing, a lock SPIN still finds an error in, an invariant that does not catch the broken lock, or a model that still has a counterexample. Send the work back with a reason if it needs more.

The definition on GitHub

The file is the whole lab definition, the same text the platform runs: size, setup script, the helper commands, README and check. Copy it and change the problems to make a longer lab.

Try this lab, and what it costs

A free personal account can work through the basic lessons in this lab, with enough free credit each month to follow most lessons and no card. For a class, a school or college has its first 365 days free for up to 50 students, then pays per student a year, with every lab included and staff free.

Questions people ask

Does the lab need a licence?
No. Z3 is MIT, SPIN is BSD, the TLA+ tools are MIT and Alloy is Apache 2.0, with solvers under their own open licences inside its jar. They are installed on the student’s VM when it starts, and we distribute none of them.
Can a student without an account do it?
Parts one and two, Z3 and SPIN, yes. A VM with no account reaches Ubuntu’s archive and nothing else, so TLA+ and Alloy cannot be downloaded there. A signed-in student’s VM reaches GitHub and gets all four.
Can students harm anything?
Only their own copy. The tools check models and run nothing of anybody else’s. If a student breaks a file, the stock copy is in /usr/share/formallab.
Was the lab tested in a real student VM?
The setup, the lesson’s commands and the check were run in a real Ubuntu 26.04 container standing in for the VM, and the check was shown to fail on each way of faking each part and to pass with the reference solution. A booted student VM, and the download through the platform’s proxy, are worth one try before a class.