The TLA+ ecosystem

There are a number of resources in the ecosystem. The most important are

  1. The language itself
  2. Apalache - a symbolic bounded model checker
  3. TLC - an explicit state model checker

The Apalache and TLC model checkers each have pros and cons that make them suited for evaluating different models.

There are common names you will see repeatedly as you learn TLA+. We use the following

  1. VSCode Plugin - highlights and shows syntax errors, runs TLC
    We recommend using this.
  2. TLA+ standard modules - the standard library
    These modules are automatically found by Apalache and TLC when you include them.
  3. Google Group - the official discussion forum for TLA+
    It’s worth searching here if you’re stuck.
  4. tlaplus repository issues - the issues for the TLA+ components maintained by Microsoft
    It’s worth searching here if you’re stuck.

Additional keywords you might see, but that we don’t use in the basic tutorials:

  1. Modelator - a tool for model-based testing using TLA+ models
    modelator can generate hundreds of tests from a model and run them against your real system.
  2. SANY - the canonical TLA+ parser used by TLC and Apalache
    You don’t need to worry about using SANY on its own.
  3. Toolbox - a bespoke IDE for writing TLA+ and running TLC.
    The toolbox has unique features useful in niche circumstances. We recommend trying the toolbox only after getting used to TLA+, if you need to.
  4. TLA+ community modules - additional modules contributed by the community
    Using them may require downloading and providing the path for the package.
  5. Pluscal - another language which translates to TLA+
    Pluscal is less expressive than TLA+ and uses a different syntax. There are Pascal and C-like flavours. You have to translate it to TLA+ using a transpiler before checking a model written in it. We recommend trying it only after getting used to using regular TLA+.
  6. Specifying Systems - a book on TLA+ written by Leslie Lamport, original creator of TLA+
    It contains useful information on niche features of TLC and TLA+.

Footnote

Please note there are many more tools and works in the ecosystem. This page contains a basic subset.