One of a handful of small TLA+ specs that take a real-world industrial control system and ask what the minimum state machine is that keeps the system from killing someone. It sits next to the laptop power-state spec and the Dexcom G7 spec: same flavor, different system. The failure mode here is concrete. A person physically walks inside a room-sized oven, and then the oven heats up.
The interactive microwave page is a gentler introduction to TLA+. In short: a system is described as a set of variables, a set of actions that change those variables, and an invariant that should hold in every reachable state. The TLC model checker then explores every possible execution and reports whether the invariant ever breaks. Every possible execution includes the ones a human would never think to test, such as the off-by-one ordering of events that turns out to be the bug.
A walk-in oven (the kind used for curing coatings, drying lumber, baking large food batches) is a room with a heating element and a door. The dangerous configuration is straightforward: a human is inside, and the temperature is above ambient. The spec tracks three variables (temp, door, and inside) and six actions: Heat, Cool, OpenDoor, CloseDoor, Enter, Exit.
The interlock that does the real work is on Enter:
Enter ==
/\ door = "open"
/\ inside = FALSE
/\ temp = MinTemp
/\ inside' = TRUE
/\ UNCHANGED <<temp, door>>
A person can step inside only if the door is open and the oven is at MinTemp. The safety invariant that the model checker tries to falsify is:
Inv4 == inside => temp = MinTemp
If any reachable state has someone inside while the temperature is above minimum, TLC reports a counterexample with the exact trace that got there. With the spec as written, it does not. Heat is guarded on inside = FALSE, so the heating element cannot turn on while someone is in the chamber. That is the point of the exercise: encode the interlock, then let the checker confirm that no path violates it.
The real-world story being modeled is the obvious one. A technician walks in to check or clean the chamber, the door swings shut, the controller resumes its program, and the chamber heats with someone inside. Walk-in ovens have physical interlocks and lockout-tagout procedures against this. The spec states those interlocks as the property that no reachable state has inside true and temp above minimum, and TLC proves it. Weakening any of the guards, for instance dropping the inside = FALSE precondition on Heat, makes the checker produce a trace showing exactly how a person ends up inside a heating oven.
This is a study spec, not a verified industrial controller. The temperature is a single integer ticking up and down by one. There is no notion of multiple people, no ventilation, no emergency stop, no temperature sensor failure, no door-stuck-open behavior. The config (TargetTemp = 20, MaxTemp = 100, MinTemp = 0) is dimensionless, chosen to give TLC a finite state space to explore rather than to model real Celsius. The whole module is under 90 lines and the README is one sentence long. It came out of the same arc of work that led into Eric Spencer's ai4fm research on getting LLMs to generate TLA+, and it doubles as an example system for explaining what TLA+ buys on a system a person can picture.
The repo is at EricSpencer00/tla-walk-in-oven: the spec is Oven.tla and the config that feeds it to TLC is Oven.cfg. With the TLA+ Toolbox or tla2tools.jar installed, it runs in seconds.