cloudparts

TLA+

Leslie Lamport’s language for specifying concurrent and distributed systems as simple mathematics, with tools that check the designs: the TLC and Apalache model checkers and the TLAPS proof system.

TLA+ Foundation project
What it is
Formal methods
Type
Open source
Made by
TLA+ Foundation (Linux Foundation), created by Leslie Lamport
Foundation
TLA+ Foundation, joined January 2023. Part of the Linux Foundation
License
MIT (TLC and the other core tools, VS Code extension); TLAPS: BSD 2-Clause; Apalache: Apache 2.0
Facts checked
28 October 2026
Website Source code

What it is

A TLA+ specification describes a system as a state machine. You declare its variables, write Init, a formula saying what the initial states are, and Next, a disjunction of actions, each a formula that relates the current state to the next one, where a primed variable such as x' means its value after the step. Spec == Init /\ [][Next]_vars then describes every behaviour the system allows. Properties are formulas too: invariants such as “no two nodes hold the lock”, and temporal properties such as “every request is eventually answered”, which need fairness assumptions. Modules can EXTEND and INSTANCE each other, so you can show that a detailed design refines a simpler one. Programmers often start with PlusCal instead, a pseudocode-like algorithm language written in a comment that a translator turns into TLA+.

The core tools ship as one Java archive, tla2tools.jar (Java 11 or later): the SANY parser, the PlusCal translator, TLATeX, a REPL and TLC. TLC is an explicit-state model checker. A configuration file names the specification, gives the constants small values (three servers, two client requests) and lists the invariants and properties; TLC then visits every reachable state on all cores, or samples random behaviours in simulation mode, and prints a step-by-step trace when a property fails. Apalache checks the same language symbolically, translating it into constraints for the Z3 or CVC5 SMT solvers, which suits large data domains, bounded runs and inductive invariants. TLAPS, the proof system, checks hierarchical proofs written in TLA+ by sending each obligation to Z3, Zenon, Isabelle/TLA+ or LS4, and covers every instance size rather than the few a model checker can visit.

The recommended editor is now the TLA+ extension for VS Code and compatible editors, which runs the parser and TLC; the Eclipse-based TLA+ Toolbox is no longer maintained. Since 2023 the TLA+ Foundation at the Linux Foundation has owned the language: its Specification Language Committee decides changes to TLA+, and the code lives in the tlaplus GitHub organisation, with Apalache in its own project since 2026. Tagged releases are rare; the last full release of the tools was 1.7.4 in August 2024, and newer versions are published as a 1.8.0 pre-release and rolling builds that are rebuilt as changes land.

Why teams pick it

  • Finds design bugs that need long, unlikely sequences of events: AWS’s DynamoDB model produced a data-loss trace 35 steps long, after the design had passed reviews, code reviews and testing
  • Proven in industry: AWS since 2011, Azure Cosmos DB, MongoDB, Oracle Cloud Infrastructure (hundreds of specifications across dozens of services) and Datadog, among others
  • One language, three ways to check it: exhaustive TLC for small instances, symbolic Apalache, and TLAPS proofs for all sizes
  • Abstraction is built in: a specification leaves out everything the property doesn’t depend on, and refinement links a detailed design to a simple one

Watch out for

  • It checks the specification, not your code: nothing ties the two together unless you add trace validation, and a spec kept by hand drifts as the system changes
  • TLC is exhaustive only for the small constants you choose, and the state space grows exponentially; big models need many cores (AWS once ran distributed TLC on ten EC2 instances), and TLC can’t handle integers above 2³¹ − 1
  • Unfamiliar notation of sets, functions and temporal logic: AWS engineers needed two to three weeks to get useful results, and teams often start in PlusCal instead
  • A small maintainer base: the Toolbox is unmaintained, tagged releases are years apart, and much of the work rests on a few people and foundation grants

How it fits with other technologies

The same lost-update race in PlusCal, translated and checked from the command line · text

---- MODULE Counter ----
EXTENDS Naturals
(* --algorithm counter
variables x = 0;
process worker \in {1, 2}
variables tmp = 0;
begin
  Read:  tmp := x;
  Write: x := tmp + 1;
end process;
end algorithm; *)
\* BEGIN TRANSLATION ... END TRANSLATION  (written here by pcal.trans)

BothCounted == (\A w \in {1, 2} : pc[w] = "Done") => x = 2
====

\* Counter.cfg:   SPECIFICATION Spec   INVARIANT BothCounted
\* $ java -cp tla2tools.jar pcal.trans Counter.tla    (PlusCal to TLA+)
\* $ java -jar tla2tools.jar -workers auto Counter.tla
\*   Error: Invariant BothCounted is violated.  (followed by the trace)

See it in a real stack

No architecture uses TLA+ yet. Drop it into the playground and wire it up yourself.Open playground →
Where it came from1994–2026

Leslie Lamport had worked on concurrent and distributed algorithms since the 1970s, and wanted a way to state them precisely enough to check. His Temporal Logic of Actions, published in 1994, describes a system by the steps it may take. TLA+ added sets, functions and modules on top, and in 1999 Yuan Yu, Panagiotis Manolios and Lamport described TLC, a model checker for it. The book Specifying Systems followed in 2002. Hardware engineers were early users: a DEC/Compaq team verified cache-coherence protocols for Alpha processors, and Intel used TLA+ on cache-coherence designs before writing RTL.

Lamport developed TLA+ further at Microsoft Research. He added PlusCal in 2009 for people who think in pseudocode, an Eclipse-based Toolbox appeared in 2010, and the TLA+ Proof System was built at the Microsoft Research–Inria Joint Centre and presented in 2012. Meanwhile AWS adopted TLA+ in 2011 and wrote about it in Communications of the ACM in 2015, which brought the language to many cloud and database teams. In 2021 a VS Code extension arrived, and in March 2022 Apalache, a symbolic model checker started at TU Wien and developed at Informal Systems, became available.

In 2023 TLA+ moved to the Linux Foundation: the TLA+ Project became a series of LF Projects in January, and the TLA+ Foundation was launched in April. Lamport retired from Microsoft on January 3, 2025 and wrote that TLA+ is “now under the control of the TLA+ Foundation”. Foundation grants pay for work such as moving TLAPS onto the SANY parser, and Apalache joined the foundation as its own LF Projects series in 2026.

Why it’s built this way

Mathematics instead of a programming language
Lamport’s premise is that “the best way to describe things precisely is with simple mathematics”, which lets a specification describe what a system may do without saying how the code does it.
PlusCal as a front end
Many engineers find a pseudocode-like algorithm easier to start with; AWS observed that engineers “often find it easier to begin with PlusCal”, and its translator produces ordinary TLA+ for the same tools.
Several independent checkers
Explicit-state checking finds bugs quickly in small instances but can’t prove a design for all sizes, so TLC, Apalache and TLAPS each cover a different trade-off between automation and generality.
Handing the language to a foundation
After decades under Lamport’s stewardship with Microsoft’s support, a Linux Foundation project with a language committee and paying members gave TLA+ a future that doesn’t depend on one person or company.

Timeline

  1. 1994

    “The Temporal Logic of Actions” is published in ACM TOPLAS

  2. 1999

    TLC, the TLA+ model checker, is described at CHARME

  3. 2002

    Specifying Systems, the TLA+ book, is published

  4. 2009

    PlusCal, the algorithm language that translates to TLA+

  5. 2012

    The TLA+ Proof System is presented at FM 2012

  6. 2021

    A VS Code extension becomes available in January

  7. 2023

    The TLA+ Foundation launches at the Linux Foundation on April 21

  8. 2026

    Apalache becomes a TLA+ Foundation project

Sources12 · facts checked 28 October 2026

Improve this page on GitHub