An integrated development environment for writing and checking TLA+ specifications.
TLA (the Temporal Logic of Actions) is a logic for specifying and reasoning about concurrent and reactive systems. It is the basis for TLA+, a complete specification language.
...