TLC
Formal verification · the first TLA+ checker
created · updated
The first program that checks TLA+ models. It goes through all states of a model one by one and checks the rules in each, remembering where it has been. So its work is predictable, but the world of the model must be small: otherwise there are too many states. Quint models can be checked in TLC too, but they first have to be translated into a form this program accepts.
Source: TLA+ Tools and TLC on GitHub
Where it appears · 2
- How model checking differs from testing · Specs and context
- TLA+ vs Alloy vs Quint · Specs and context