TLA+ (Temporal Logic of Actions): Specification Language and TLC Guide

TLA+ (Temporal Logic of Actions) is a formal specification language for describing concurrent and distributed systems precisely enough that a tool can check the design before any code is written. Searchers for “TLA+” mostly want one of three things: what the abbreviation means, what a TLA+ specification looks like, or how to start running the checker. This page covers all three and ends with the official sources.

What does TLA stand for in software?

In software, TLA stands for Temporal Logic of Actions, the logic on which the TLA+ language is built. Leslie Lamport’s TLA+ home page describes TLA+ as “a high-level language for modeling programs and systems–especially concurrent and distributed ones,” based on the idea that simple mathematics is the best way to describe things precisely (read 2026-11-07).

You searched for	Usually means	Covered here?
TLA+ , TLA+ specification, TLC model checker	The formal specification language and its tools	Yes
TLA Philly, TLA South Street, TLA tickets	A live-music venue	No
TLA in an organisation name	Initials of that organisation (for example a library association)	No
TLA as “three-letter acronym”	The general jargon term for a three-letter abbreviation	No

What does TLA mean in the army?

This page is about the specification language only. A military meaning of the abbreviation is unrelated to TLA+ and is not covered here; check the glossary of the service or organisation that used it.

What it is used for in research

The language targets design errors in concurrent and distributed systems, which the TLA+ home page notes are hard to find and expensive to fix once they are in code. In research settings this means writing a short mathematical model of a protocol or algorithm and letting a tool explore its possible behaviours. A specification is a research artefact in its own right: it can be versioned, archived and cited alongside the paper that describes the algorithm (see FAIR4RS and reproducibility infrastructure).

What are TLA+ specifications?

A TLA+ specification is a module that defines a system as a set of allowed behaviours (sequences of states). The usual structure has four parts:

• Variables that hold the system state.
• An initial-state predicate (conventionally named Init) that says which states a run may start in.
• A next-state relation (conventionally Next) that says which state changes are allowed; primed variables such as x' denote the value after the step.
• Properties to check: invariants (something true in every reachable state) and, for liveness, temporal properties (something that must eventually happen).

A minimal illustrative module, a counter that cycles through 0 to 3:

---- MODULE Counter ----
EXTENDS Naturals
VARIABLE x

Init   == x = 0
Next   == x' = (x + 1) % 4
TypeOK == x \in 0..3

Spec   == Init /\ [][Next]_x
====

A matching configuration file, Counter.cfg, tells TLC what to check:

SPECIFICATION Spec
INVARIANT TypeOK

This example is a teaching sketch written for this page, not taken from the official documentation. The home page also points to PlusCal, an algorithm language that is translated into TLA+, for people who prefer a pseudocode-like notation.

Install or access (official source only)

The tools are published as GitHub releases of the tlaplus/tlaplus repository. As read on 2026-11-07 the latest stable release was v1.7.4 (“The Xenophanes release”), and v1.8.0 (“The Clarke release”) was marked as a pre-release. Re-check the releases page before relying on a version number.

• tla2tools.jar is a release asset containing TLC; it needs a Java runtime.
• The Toolbox is an integrated development environment for TLA+; v1.7.4 ships zip files for Windows, Linux and macOS. The releases page states that the Toolbox “is no longer actively maintained” and lists the TLA+ extension for Visual Studio Code and compatible editors as an actively maintained alternative.
• VS Code extension: listed on the Visual Studio Marketplace and linked from the TLA+ home page.

Step-by-step: check a specification with TLC

1. Save the module above as Counter.tla (the file name must match the module name) and the configuration as Counter.cfg in the same folder.
2. Download tla2tools.jar from the releases page and confirm a Java runtime is installed.
3. From that folder run TLC through its main class:

   java -XX:+UseParallelGC -cp /path/to/tla2tools.jar tlc2.TLC -workers auto Counter.tla

4. For the full list of options run java -cp /path/to/tla2tools.jar tlc2.TLC -h.

Two flags come from the release notes: the notes ask command-line users to always pass -XX:+UseParallelGC with Java 11 to avoid a performance penalty, and -workers auto sets the number of worker threads from the available parallelism. To use the Toolbox or the VS Code extension instead, create the module and model there and run TLC from the menu.

Output and how to read it

TLC is, in the words of Lamport’s tools page, “an explicit-state model checker that can check both safety and liveness properties”; it can also act as a simulator for executable specifications. Explicit-state means it enumerates the reachable states one by one. For the counter above, the state space is the four values of x, so a run should finish quickly with no error. When a property is violated, TLC stops and reports which property failed together with a sequence of states from an initial state to the violation (an error trace), which is the most useful output for debugging a design. TLC does not prove the specification correct in general: it checks the finite model you give it. The companion proof system, TLAPS, is “a system for mechanically checking proofs written in TLA+.”

Troubleshooting

• Slow runs on Java 11: add -XX:+UseParallelGC as the release notes advise.
• Errors on an old Java: the release notes record fixes for class-loading errors on Java 1.8 and for a startup crash on newer Java in older builds; update to the latest stable release.
• Liveness results with several workers: v1.7.4 fixes a soundness problem where liveness checking with multiple workers could fail to report a violation, so do not use an older build for liveness properties.
• File not found: the module name inside the file must match the .tla file name.

Free alternatives and companions

Tool	What its own site says	Relation to TLA+
Alloy	“an open source language and analyzer for software modeling”; version 6.2.0 released 2025/01/09 (read 2026-11-07)	A different modelling language, not a TLA+ tool
Apalache	“The Symbolic Model Checker for TLA+”; translates specifications into the logic supported by SMT solvers such as Z3	A second checker for TLA+ specifications, an alternative to TLC rather than a rival language

How to learn TLA+?

Start with the official Learning TLA+ page, which lists: the TLA+ Video Course (for readers with basic programming knowledge; it does not cover PlusCal); a 14-session PlusCal tutorial; Hillel Wayne’s LearnTLA site and book Practical TLA+; the PlusCal manuals; the book Specifying Systems, which describes TLA+ and TLC as of 2002 (the page notes the language has changed since); and the unfinished TLA+ Hyperbook. A practical order is the video course first, then specify a small protocol you already understand and check it with TLC. For the wider habit of treating specifications and code as research outputs, see software engineering for research and the research software engineer role; for peer inspection of such artefacts, see code review (research software).

FAQ

What does TLA stand for in software?

Temporal Logic of Actions, the logic underlying the TLA+ specification language.

What are TLA+ specifications?

Mathematical descriptions of a system’s variables, initial states and allowed state changes, plus the properties it must satisfy, which the TLC model checker can explore automatically.

How to learn TLA+?

Use the video course and other resources on Lamport’s official learning page, then practise by specifying a small protocol and checking it with TLC.

What does TLA mean in the army?

That meaning is unrelated to TLA+ and is not covered on this page.

Sources (official docs)

• The TLA+ home page, Leslie Lamport, read 2026-11-07.
• TLA+ tools page, read 2026-11-07.
• Learning TLA+, read 2026-11-07.
• tlaplus/tlaplus releases, read 2026-11-07.
• Alloy and Apalache project sites, read 2026-11-07.