Posts tagged Stuttering
Interactive Microwave: TLA+ in the Browser
- 17 April 2026
We published a browser-native version of the
interactive-microwave-tla
simulator. It mimics a Java microwave runtime and a small TLA+ model checker
that is a literal transcription of the project’s Microwave.tla spec, so
students can experiment with the state machine — including the stuttering
liveness failure from Laufer, Mertin, and Thiruvathukal,
arXiv:2407.21152 — without installing
Java, Maven, or TLC.