Hands-on challenges for writing formal specifications, running the TLC model checker, and visualizing state spaces — all in your browser.
Write Specs
Author TLA+ specifications in a focused in-browser editor.
Run TLC
Check your model with TLC and get instant, detailed feedback.
Visualize States
Explore the state-space graph to understand system behaviour.