Guix

TLA+ is a high-level language for modeling programs and systems---especially concurrent and distributed ones. It's based on the idea that the best way to describe things precisely is with simple mathematics. TLA+ and its tools are useful for eliminating fundamental design errors, which are hard to find and expensive to correct in code.

The following TLA+ tools are available in this distribution:

• The Syntactic Analyzer: A parser and syntax checker for TLA+ specifications;

• TLC: A model checker and simulator for a subclass of "executable" TLA+ specifications;

• TLATeX: A program for typesetting TLA+ specifications;

• Beta test versions of 1-3 for the TLA+2 language; and

• The PlusCal translator.