TLC ships as one jar with six entry points, and the in-repo Toolbox GUI is called unmaintained

One jar, six entry points, and a bare java run that reaches only TLC

Everything ships in a single file. `tla2tools.jar`, taken from the releases page, carries multiple tools at once, and once it sits on the classpath each one is started by its own main class:

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

The split between the parser and the checker is the part worth knowing. `tla2sany.SANY` parses a specification, `tlc2.TLC` checks a model, and `tla2sany.xml.XMLExporter` writes that parse tree out as XML, so a specification can be syntax checked without ever reaching the model checker.

There is a shortcut, and it is narrower than it looks. Running `java -jar tla2tools.jar` is aliased to run `tlc2.TLC`, so the default entry point in the jar is the model checker and nothing else. The REPL, the PlusCal translator and the LaTeX translator only start when their class names are spelled out.

The description names the Toolbox as an IDE, and the same page calls it unmaintained

The repository description names two products: TLC, a model checker for specifications written in TLA+, and the TLA+ Toolbox, an IDE for TLA+. Both are hosted here.

Only one of them is described as alive. For graphical use the README points at the TLA+ VS Code extension, which is a separate repository. The Eclipse based Toolbox GUI, it adds, is also available from this repository but is currently unmaintained.

So the IDE named in the description is the one flagged as not being worked on, and the maintained graphical route is the extension hosted next door. Anyone choosing a front end is choosing between another project and a desktop application that is not being patched. Anyone choosing a checker is unaffected by that sentence: `tlc2.TLC` is the tool the release cadence and the pre-release pipeline are built around, and the Toolbox statement does not touch it.

The classpath line in the README uses an uppercase command

The snippet that sets up the classpath reads `EXPORT CLASSPATH=tla2tools.jar`. `export` is the shell builtin; `EXPORT` in uppercase is not one, so pasted into a POSIX shell that line does nothing and every tool started afterwards fails to resolve. The surrounding prose states the requirement correctly, that `tla2tools.jar` must be added to the classpath, which makes the capitalisation read as a slip inside the fence rather than a documented alternative.

The path is relative too. With the jar named without a directory, the classpath resolves only while your shell is sitting next to the file. There is no launcher script or wrapper at the top level to hide that; the entries there are the two source trees, the build file, and the project documentation.

Both details are cheap to work around and cheap to miss. Write the line with the builtin in lower case, and either keep the jar alongside the shell or put an absolute directory into the variable before running any of the six classes from elsewhere.

Every master commit is republished as the Clarke pre-release

There are three ways to consume this project, and they sit at different levels of stability.

The releases page holds versioned releases. The current one is v1.8.0, named The Clarke release, published on 2026-10-04. The two before it are v1.7.4, The Xenophanes release, and v1.7.3, The Ulpian release, both dated 2024-08-05.

Over the top of that, every commit to the master branch is built and uploaded to the v1.8.0 Clarke pre-release, and the README says that if you want the latest fixes and features, that is the one to use. The v1.8.0 tag is therefore not a fixed point: the artifacts hanging off it move as master moves.

Java consumers get a third channel. Maven packages are published periodically to Sonatype under `org.lamport.tla2tools` at version `1.8.0-SNAPSHOT`, so a dependency declaration tracks the same rolling code by a different route.

v1.7.3 and v1.7.4 landed 23 minutes apart, then the line went quiet for two years

v1.7.3, The Ulpian release, was published on 2024-08-05 at 19:53 UTC. v1.7.4, The Xenophanes release, followed the same day at 20:16 UTC. A patch and a minor released back to back reads like a hurried correction rather than a scheduled plan.

After that, nothing new for more than two years. The next tag, v1.8.0, The Clarke release, is dated 2026-10-04. The master branch itself was last pushed on 2026-10-02, so the repository was already moving two days before that tag was published, which is consistent with the arrangement described above: master lands in the Clarke pre-release continuously, and the version number only catches up at a release.

Each release carries a name borrowed from a philosopher. Ulpian, Xenophanes, Clarke. That naming is the tidiest thing about the release history, and the gap between Ulpian and Clarke is the rest of it.

One Maven root holds the tools tree and the Eclipse toolbox tree

The build is a single Maven project with `pom.xml` at the repository root. Beneath it, `tlatools/` holds the tools source in `org.lamport.tlatools`, and `toolbox/` holds the Toolbox IDE, which is based on the Eclipse Platform rather than on Maven conventions.

Also at the top level: `.devcontainer/`, `.github/`, `docs/`, `general/`, a `keystore` directory, a `CNAME` file, and three documents. `USE.md` covers using and consuming the tools, `DEVELOPING.md` covers building and testing them plus setting up a development environment, and `CONTRIBUTING.md` is the process one.

Two of those are worth a second look. The `keystore` directory sits next to the build file, and nothing in the README explains what it holds or when it is consulted, so anyone wiring up their own signing has no reference to compare against. The `CNAME` file at the root is a custom domain record of the kind GitHub Pages uses, and the README separately points readers to http://tlapl.us for TLA+ itself.

Contributing is gated because the models end up in safety-critical systems

One README line does the work of a governance document: TLA+ is used in safety-critical systems, so a contribution process is in place to ensure quality is maintained, and contributors are asked to read CONTRIBUTING.md before beginning work.

That is the whole stated reason. No review latency, no test requirement and no commit format are described in the README itself; those belong to the process document it points at.

Development of the project is managed by the TLA+ Foundation, and the proof manager, the separate tool for the proof side of TLA+, sits at its own site rather than in this repository. The wider arrangement is therefore split into pieces: the language, the checker, the proof manager and the foundation are distinct, and this repository holds the command line tools plus the desktop IDE.

Editorial conclusion

This repository is worth taking for the command line tools and treating with suspicion as a desktop product. `tlc2.TLC` and the rest of tla2tools.jar are the path that gets maintained, the Clarke pre-release tracks master continuously rather than marking a fixed version, and the Toolbox IDE shipped here is described as unmaintained. Before depending on it, decide which of the three consumption channels you actually want: a tagged release, a pre-release that moves with every master commit, or a Sonatype snapshot. If you need a graphical environment, budget for the separate VS Code extension rather than the IDE in this repository.

Frequently asked questions

Official sources

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