tlakit · LUC-AI4FM
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.