tlakit · LUC-AI4FM

Check a
TLA⁺ specification.

Paste a module, name an invariant, and TLC will look for a behaviour that breaks it. If it finds one you get the counterexample — every state, the action that caused each step, and which variables changed.

Specifications run with tla2tools alone. The standard modules are pure, so a spec submitted here has no way to read a file, open a socket, or run a command.

Specificationmodule

Configuration.cfg

state space ⌘ ↵ to run

Or from a terminal

Upload the file rather than escaping it into JSON — a TLA⁺ module is mostly newlines, backslashes and quotes.

curl -F spec=@Counter.tla -F cfg=@Counter.cfg \
  https://tla-runner.ericspencer.us/check

cfg is optional. POST /parse takes a spec the same way and runs SANY only — no state space, so it answers in milliseconds. The JSON form ({"spec": "...", "config": "..."}) still works everywhere.