Introduction to TLA+
Relevant source files
The following files were used as context for generating this wiki page:This repository is a collection of TLA⁺ specifications and models that serve as a comprehensive example library, a test corpus for TLA⁺ language tools, and a set of case studies for applying formal specification. TLA⁺ is a formal specification language used to design, model, document, and verify concurrent and distributed systems. The examples cover a wide variety of fields and algorithms, from beginner-friendly puzzles to complex protocols like Paxos.
The specifications (.tla files) are validated using a suite of tools to ensure correctness and maintain a high standard of quality. The primary tools used are the TLC model checker, the Apalache symbolic model checker, and the TLAPS proof system. Many specifications also include PlusCal, a high-level algorithmic language that transpiles to TLA⁺. This ecosystem allows for rigorous analysis of system designs, checking for properties like safety, liveness, and refinement.
Sources: README.md:1-11, CONTRIBUTING.md:3-7
Getting Started with TLA+ and the Examples Repo
To begin working with the TLA⁺ specifications in this repository, you should first install the TLA⁺ Toolbox. The recommended version is a pre-release from the nightly builds, which contains the latest features. Once the Toolbox is installed, you can open a specification by navigating to File > Open Spec > Add New Spec... and selecting the root .tla file of the algorithm you wish to study.
Sources: specifications/PaxosHowToWinATuringAward/README.txt:20-29
The typical workflow for learning from an example involves:
- Viewing the Spec: Read the TLA⁺ source files (
.tla) and any accompanying documentation. Many specs include pretty-printed PDF versions to aid understanding. - Running the Model Checker: Use the provided models (
.cfgfiles) to run the TLC model checker. This helps in understanding the algorithm's behavior. - Experimenting: The models often include small exercises, such as modifying the spec to introduce an error and observing if TLC can find it. This is a crucial step in verifying that the specification correctly models the intended algorithm.
Sources: specifications/PaxosHowToWinATuringAward/README.txt:31-43
This diagram illustrates the initial learning process.
Core Concepts and Tools
The repository utilizes a set of core TLA⁺ concepts and tools for specification and verification.
| Component | Description |
|---|---|
Specification (.tla) | A file containing the formal description of a system or algorithm written in TLA⁺. |
Model (.cfg) | A configuration file that tells the TLC model checker what to check, including invariants, properties, and constants. |
| PlusCal | An algorithm language that is easier to write for many and translates into a TLA⁺ specification. Indicated by a pluscal feature tag. |
| TLC | The explicit-state model checker for TLA⁺. It explores the state space of a specification to check for violations of safety and liveness properties. |
| Apalache | A symbolic model checker for TLA⁺ that can check properties on infinite state spaces. |
| TLAPS | The TLA⁺ Proof System, used to mechanically check deductive proofs written in TLA⁺. |
Sources: README.md:12-20, CONTRIBUTING.md:13-17, DEVELOPING.md:27-33
The Specification Development and Validation Workflow
Contributing a new specification to this repository involves a structured process that ensures quality and consistency through automated validation.
Contribution Flow
The process for adding a new spec is as follows:
- Create Spec Directory: Fork the repository and create a new directory for your specification under
specifications/. - Add Files: Place all TLA⁺ (
.tla) and model configuration (.cfg) files in this directory. - Create
manifest.json: Add amanifest.jsonfile that contains metadata about the spec, including authors, sources, and details about the models (runtime, expected result, etc.). This can be auto-generated using a provided script. - Update
README.md: Add an entry for your spec in the main table inREADME.md, ensuring the details match themanifest.json. - Open Pull Request: The CI system will automatically run a series of validation scripts against the new spec.
Sources: CONTRIBUTING.md:10-33
This diagram shows the contribution and continuous integration workflow.
Sources: CONTRIBUTING.md:10-77, DEVELOPING.md:8-36
CI Validation Scripts
The repository uses a comprehensive set of scripts to validate every contributed specification.
| Script | Purpose |
|---|---|
check_manifest_schema.py | Validates manifest.json files against the defined schema. |
check_manifest_files.py | Ensures modules and models in manifest.json match the actual files. |
check_manifest_features.py | Uses tree-sitter-tlaplus to verify that features like proof and pluscal are correctly recorded. |
check_markdown_table.py | Validates that the README.md table is consistent with the manifest.json files. |
translate_pluscal.py | Runs the PlusCal translator on all modules containing PlusCal code. |
parse_modules.py | Runs the SANY parser on all .tla files to check for syntactic and semantic validity. |
check_small_models.py | Runs TLC or Apalache on models expected to complete quickly, verifying their outcomes. |
smoke_test_large_models.py | Runs larger models for a short duration (5 seconds) to ensure they don't crash immediately. |
check_proofs.py | Runs TLAPM to validate formal proofs in modules that contain them. |
Sources: DEVELOPING.md:8-36
Writing and Checking a Specification
The goal of writing a TLA⁺ spec is to create a correct and unambiguous description of an algorithm. A key practice is to use the TLC model checker not just to prove correctness, but also to find flaws. You know you have written a correct spec if TLC reports that it violates a property, and upon examining the error trace, you discover an error in the algorithm itself, rather than a mistake in your specification.
If TLC finds no error, it could mean the algorithm is correct, or that the spec isn't describing what you think it is. To gain confidence, a good technique is to intentionally introduce a small modification that should break the algorithm and verify that TLC finds the expected error.
Sources: specifications/PaxosHowToWinATuringAward/README.txt:48-59
The interaction between a developer and TLC can be visualized as follows:
Advanced Concepts
Beyond basic safety and liveness checking, TLA⁺ is used for more advanced verification techniques within this repository.
Refinement
Refinement is a technique to prove that a detailed, low-level specification (the implementation) correctly implements a simpler, high-level specification (the abstraction). This is a powerful way to manage complexity. The ewd998 specification demonstrates a chain of refinements, where each spec adds more detail while being proven to conform to the one above it.
This diagram shows the refinement hierarchy for the EWD998 termination detection algorithm.
The locks_auxiliary_vars example demonstrates a two-way refinement using auxiliary variables, proving that Peterson's algorithm refines an abstract lock specification.
Sources: specifications/locks_auxiliary_vars/README.md:4-8
Simulation for Statistical Analysis
TLA⁺ and TLC can also be used for more than just finding correctness violations. The ewd998 example explores using TLC's simulator to generate random execution traces. By analyzing a large number of these traces, one can infer statistical properties about the system's performance, such as the average number of steps to detect termination under different algorithmic variants. This allows for performance analysis at the design level, before writing any implementation code.
Sources: specifications/ewd998/README.md:40-52
Conclusion
The TLA⁺ Examples repository serves as a critical resource for the TLA⁺ community. It provides a rich collection of well-documented and validated specifications that demonstrate how to model and verify a wide range of systems. By leveraging tools like TLC, Apalache, and TLAPS, and employing techniques from basic model checking to advanced refinement and simulation, the repository showcases the power of formal methods in building reliable and correct software systems. The structured contribution and validation process ensures that it remains a high-quality, living library of formal specification case studies.
Sources: README.md:4-8, CONTRIBUTING.md:3-7