Why TLA+ Is the Secret Weapon for Verifying Distributed Systems

1. Introduction

Nuwa is the foundational distributed‑cooperation service in Alibaba Cloud, supporting almost all cloud products such as compute, networking, and storage. Its consistency engine implements protocols like Paxos, Raft, and EPaxos, and guaranteeing the correctness of this engine is a major challenge. Tools such as TLA+ and Jepsen are introduced to ensure the consistency library works correctly.

2. Overview of TLA+

TLA+ (Temporal Logic of Actions), created by Leslie Lamport, is a formal verification language for designing, modeling, documenting, and verifying programs, especially concurrent and distributed systems. It uses simple mathematical theory to describe systems precisely, helping eliminate hard‑to‑find bugs.

To verify a program with TLA+, one first writes a specification, then runs the TLC model checker, which exhaustively explores all possible behaviors and checks the specified properties.

Because TLA+ is based on mathematics, Lamport also created PlusCal, a language that looks like a regular programming language, making it easier for engineers to write specifications that can be automatically translated into TLA+.

3. TLA+ Applications

TLA+ is widely used in both academia and industry. Many distributed‑algorithm papers include TLA+ specifications to prove correctness. Practitioners often find TLA+ specifications faster to understand than lengthy paper descriptions, and the specifications serve as precise implementation guides.

On the industry side, Amazon AWS uses TLA+ to verify core algorithms of several critical services; the tool has uncovered serious design issues that could have caused massive losses if left unchecked.

4. Getting Started with TLA+

Install the TLA+ extension for VS Code and begin with a simple example: a single‑bit clock that toggles between 0 and 1. The PlusCal description of this clock is shown below.

The PlusCal code can be translated into TLA+ code.

The resulting TLA+ specification defines the system’s behavior: Init initializes the clock, Tick toggles it, and Stutter keeps it unchanged. To run the model, save the specification as clock.tla and create a simple clock.cfg file that names the specification and the invariant to check.

Running TLC produces statistics as shown.

5. TLA+ Principles

TLA+ explores the state graph by traversing every reachable state and checking invariants at each step. It uses breadth‑first search by default, but can be configured for depth‑first or random exploration.

This exhaustive traversal ensures that safety and liveness properties of algorithms are fully verified.

6. TLA+ Concurrency

Although the model checker runs serially, TLA+ can represent concurrent or distributed algorithms whose actions are only partially ordered. By imposing a total order that respects causal relationships (as described in Lamport’s “Time, Clocks, and the Ordering of Events in a Distributed System”), TLA+ can model and verify such systems.

7. Conclusion

TLA+ leverages powerful computation to explore all possible behaviors of an algorithm, uncovering unexpected bugs. As systems grow more complex, TLA+ becomes an essential skill for engineers. For newcomers, the book “Practical TLA+” is a recommended starting point, and a free electronic version is available online.