TLA+ Tools and Toolbox: What the tlaplus/tlaplus Repository Actually Ships

What the tlaplus/tlaplus repository contains

This repository is not TLA+ itself. It hosts two things: the core TLA+ command line tools, and the Eclipse-based TLA+ Toolbox IDE. The README states that development is managed by the TLA+ Foundation and that the language's own site is tlapl.us. The proof manager lives in a separate project at proofs.tlapl.us, so anyone looking for proofs will not find them here.

The audience is narrow and specific. TLA+ is a specification language for concurrent and distributed systems, and the repository topics list algorithms, model-checking, specifications and verification. In practice the people who adopt it are engineers who want to describe a protocol or an algorithm precisely and then have a tool search the state space for counterexamples before any code exists. The README notes that TLA+ is used in safety-critical systems, which is why the project asks contributors to read CONTRIBUTING.md before starting work.

How TLC and SANY divide the work

The tools are packaged as one jar, tla2tools.jar, that exposes several entry points. SANY is the parser: it reads a TLA+ specification and reports syntax and semantic errors. TLC is the model checker: it takes a specification plus a configuration, enumerates reachable states, and checks invariants and temporal properties against them. The README lists these entry points explicitly, along with a REPL, the PlusCal-to-TLA+ translator pcal.trans, a LaTeX translator tla2tex.TLA, and an XML exporter for the parse tree.

The data flow is the part worth understanding before adopting it. You write a specification, SANY parses it into a semantic tree, and TLC explores states generated from that tree. Because TLC enumerates states rather than proving a theorem, the model you check has to be finite: constants must be instantiated with concrete small values. That is the central constraint of the whole toolchain, and it is what separates TLC from a proof assistant. A specification can be perfectly valid and still be impractical to check if the state space is too large. The repository topics mention high-performance, and TLC does run states in parallel, but the finite-model requirement does not go away.

Installing tla2tools.jar and running TLC once

The only prerequisite the README names is Java 11 or newer. There is no package manager step and no installer: you download tla2tools.jar from the releases page, put it on your CLASSPATH, and invoke the tool classes. The README gives this exact sequence.

EXPORT CLASSPATH=tla2tools.jar
java tla2sany.SANY -help  # The TLA⁺ parser
java tlc2.TLC -help       # The TLA⁺ model checker
java tlc2.REPL            # Enter the TLA⁺ REPL
java pcal.trans -help     # The PlusCal-to-TLA⁺ translator
java tla2tex.TLA -help    # The TLA⁺-to-LaTeX translator
java tla2sany.xml.XMLExporter -help # Export TLA⁺ parse tree as XML

Running each of those with -help is the fastest way to confirm the jar is on the classpath and the JVM version is acceptable. The README also notes that java -jar tla2tools.jar is aliased to run tlc2.TLC, so the model checker can be started without naming the class. For a first real use, point TLC at a specification and its configuration file; the README does not reproduce that workflow, and directs readers to USE.md for details on using and consuming the tools. Read USE.md before assuming a flag exists, because this page does not enumerate TLC's options.

If you prefer a graphical interface, the README points to the TLA+ VS Code extension in a separate repository. The Eclipse Toolbox GUI is also built from this repository, but the README states plainly that it is currently unmaintained.

The Toolbox is in the repository but not maintained

The most consequential fact in the README is one sentence: the Eclipse-based TLA+ Toolbox GUI is available from this repository but is currently unmaintained. A reader who searches for the Toolbox will find it, download it, and reasonably assume it is the intended way to use TLA+, because it is an IDE and it is listed next to the CLI tools.

It is not the intended path. The README's own recommendation for a graphical interface is the VS Code extension in a different repository. That leaves the Toolbox in an awkward position: the source is in the toolbox directory, it is built from this repository, and the top-level pom.xml ties it into the build, yet the project does not describe it as maintained. For a new user, the CLI tools plus the VS Code extension are the supported combination. For an existing Toolbox user, the repository layout suggests the code is still there, but nothing in the README promises fixes.

There is a second friction point in the same area. The README describes versioned releases on the Releases page, then says that every commit to master is built and uploaded to the 1.8.0 Clarke pre-release, and that you can use that pre-release if you want the latest fixes and features. So the newest build is a pre-release, while the most recent numbered release is v1.8.0, dated 2026-09-23. Anyone who wants a stable artifact should check which of the two they are actually downloading.

Where TLC stops being the right tool

TLC checks models, not theorems. If a property must hold for all inputs, including unbounded ones, TLC cannot establish that; it can only fail to find a counterexample within the finite configuration you gave it. That distinction matters for safety-critical work, and it is the reason the README points to a separate proof manager at proofs.tlapl.us. A passing TLC run is evidence, not a proof.

The state-space constraint is the practical failure mode. Constant instantiation with small values is what makes checking tractable, and it is also what limits what you learn. A bug that only appears with a larger configuration will not surface. Symmetry reduction and other techniques exist in the tooling, but the README does not document them here, so treat them as something to confirm in USE.md rather than assume.

There is also a build-side cost. The tools and the Toolbox are Java projects built through a Maven pom.xml, with the tool source under tlatools/org.lamport.tlatools and the IDE under toolbox/. The README notes that Maven packages are periodically published to central.sonatype.org as a snapshot, and that the version is 1.8.0-SNAPSHOT. Depending on a snapshot artifact in your own build means depending on something that is periodically published rather than released on a schedule. The README does not document rollback or a compatibility policy for those snapshots.

TLA+ versus Lean and other verification tools

The obvious comparison, and one people search for, is TLA+ against Lean. The difference is in the method, not the maturity. TLA+ with TLC is a model checker: you describe a system in a specification language built for temporal properties and concurrency, instantiate a finite model, and let the tool search for a counterexample. Lean is a proof assistant: you construct a machine-checked proof, and the result is a theorem rather than a bounded search.

That changes what you write and when. A TLA+ specification is usually short and readable by people who did not write it, which is why it fits design review of a protocol. A Lean development is a larger artifact and demands more mathematical background. TLC will find a concrete counterexample trace quickly and stop; Lean will tell you the proof is complete, or that it is not. Neither replaces the other. If your question is "does this protocol have an interleaving that violates my invariant," TLC is the direct answer. If your question is "is this property true for all n," TLC cannot answer it.

Against lighter-weight approaches, the trade-off is the same. Property-based testing exercises an implementation; TLA+ with TLC exercises a specification that has no implementation yet. That is the whole point of adopting it early, and also the reason it adds a language and a toolchain to a project rather than a test dependency.

Licence, releases and what maintenance costs

The repository is licensed under the MIT License, with copyright lines for HP Corporation, Microsoft Corporation and the Linux Foundation. MIT is permissive, so consuming tla2tools.jar as a dependency or shipping it inside a larger product is the kind of use the licence is written to allow. That is a general observation about the licence text, not legal advice; if the copyright holders or the Foundation matter to your compliance process, read LICENSE rather than a summary.

On maintenance: the repository is not archived, and the last push was on 2026-09-23. The most recent release, v1.8.0 (the Clarke release), is dated 2026-09-23, and the two before it, v1.7.4 (Xenophanes) and v1.7.3 (Ulpian), are both dated 2024-08-05. That gap is worth planning around: between mid-2024 and late 2026 there was no numbered release, even though the README says every commit to master goes into the Clarke pre-release. If your process pins a numbered version, you are pinning something that moved twice in roughly two years.

The upgrade cost sits mostly on the specification side. TLC behavior and the parser are tied to the language version, and the README does not describe a migration path between releases. For a team using the CLI tools, the practical cost is re-downloading the jar and re-running your models. For a team that embedded the tools as a Maven dependency, the cost includes tracking a snapshot version rather than a fixed release.

Editorial conclusion

Adopt tlaplus/tlaplus if you write specifications for concurrent or distributed systems and want to check them mechanically before writing code; the CLI tools are the maintained path and the Toolbox is not. Skip it if you need a general-purpose theorem prover, since TLC checks finite models rather than proving theorems. Before committing, verify that Java 11 or newer is available on your machines, read USE.md for the tool invocation details, and confirm that the pre-release tag v1.8.0 is the build you want, because every commit to master is uploaded there rather than to a numbered release.

Frequently asked questions

Official sources

1. License: MIT
2. Project website
3. README
4. Releases
5. tlaplus/tlaplus on GitHub