Anatomy of a Specification
Relevant source files
The following files were used as context for generating this wiki page:A TLA⁺ specification within this repository is a self-contained unit that formally describes and models an algorithm or system. These specifications serve as a comprehensive example library, a test corpus for TLA⁺ language tools, and a collection of case studies. Each specification is located in its own directory under the specifications/ folder and typically consists of TLA⁺ source files, model configuration files, metadata, and documentation.
The primary goal is to provide a clear, verifiable, and maintainable representation of an algorithm. This structure facilitates automated validation through a Continuous Integration (CI) pipeline, ensuring that all specifications parse correctly, their models run as expected, and their documented metadata is accurate. This rigorous approach maintains a high standard of quality across the repository.
Sources: README.md:5-11, CONTRIBUTING.md:3-7
Core Components
A specification is composed of several key file types, each serving a distinct purpose. These files work together to define, configure, document, and verify the algorithm.
This diagram illustrates the typical file structure within a specification's directory.
| File Type | Example | Purpose |
|---|---|---|
| TLA⁺ Source | EWD998.tla | Contains the formal TLA⁺ or PlusCal code defining the algorithm's logic, variables, and actions. |
| Model Config | EWD998.cfg | Configures a model for the TLC model checker, specifying constants, invariants, properties, and constraints. |
| Metadata | manifest.json | A JSON file containing structured metadata about the specification, its authors, features, and model-checking results. |
| Documentation | README.md | A Markdown file explaining the algorithm, the specification's structure, and any relevant context or publications. |
Sources: CONTRIBUTING.md:15-22, DEVELOPING.md:9-16, specifications/ewd998/README.md:13-20
TLA⁺ Source Files (.tla)
The .tla files are the heart of the specification. They contain the formal description of the algorithm written in TLA⁺. Many specifications also use PlusCal, a high-level language that transpiles to TLA⁺, to describe the algorithm in a more familiar pseudocode style.
A specification can be split across multiple .tla files. For example, a main specification like EWD998.tla might refine a more abstract one like AsyncTerminationDetection.tla. This allows for proving properties at different levels of abstraction.
Sources: specifications/ewd998/README.md:22-29, CONTRIBUTING.md:15
Model Configuration Files (.cfg)
Model configuration files, ending in .cfg, are used to run the TLC model checker on a .tla specification. They define how the model should be checked.
Key elements of a .cfg file include:
- Constants: Assigning concrete values to constants defined in the spec (e.g., the number of nodes in a distributed system).
- Invariants: Properties that must hold true in every reachable state.
- Properties: Temporal properties that the model must satisfy.
- Constraints: Assumptions about the environment or system behavior.
- View/Symmetry: Optimizations to reduce the state space during model checking.
It is a convention that the name of a .cfg file matches the .tla file it models or has its name as a prefix (e.g., Paxos.tla can have models Paxos.cfg and PaxosLiveness.cfg).
Sources: CONTRIBUTING.md:17-19, README.md:27-28, specifications/PaxosHowToWinATuringAward/README.txt:54-57
Metadata File (manifest.json)
Every CI-validated specification must have a manifest.json file in its root directory. This file provides structured metadata that is essential for automated testing, repository indexing, and user discovery. The manifest is validated against a schema to ensure its correctness.
The manifest captures details such as:
- Authors and Sources: Attribution for the spec and links to related papers or websites.
- Tags: Keywords like
"beginner"or"ewd"for categorization. - Modules: A list of all
.tlafiles in the spec. - Models: For each module, a list of associated models with their runtime, expected result (
success,safety failure, etc.), and state space statistics. - Features: Auto-detected features like the use of
pluscalorproof.
Sources: DEVELOPING.md:9-12, CONTRIBUTING.md:33-35
The following diagram shows the entity relationships within a manifest.json file.
Here is an example snippet from a manifest.json file, showing the structure for a single module and its models.
{
"path": "specifications/byzpaxos/VoteProof.tla",
"features": [
"pluscal"
],
"models": [
{
"path": "specifications/byzpaxos/VoteProof.cfg",
"runtime": "00:00:05",
"mode": "exhaustive search",
"result": "success",
"distinctStates": 6962,
"totalStates": 318877,
"stateDepth": 15
}
],
"proof": {
"runtime": "00:01:15"
}
}
Sources: specifications/byzpaxos/manifest.json:44-64
Documentation (README.md)
Each specification directory is encouraged to include a README.md file. This file serves as the primary documentation, explaining the significance of the specification, the algorithm being modeled, and providing links to relevant publications or websites. For complex specifications, the README might also explain the relationship between different .tla files (e.g., refinement mappings) and how to run the models.
Sources: CONTRIBUTING.md:21-22, specifications/ewd998/README.md:13-15, specifications/MultiPaxos-SMR/README.md:3-4
The Validation Pipeline
To ensure quality and consistency, all specifications are subject to a series of automated CI checks. Contributing a new specification involves adding it to this validation process.
The CI pipeline performs the following key steps:
- Manifest Validation: Checks
manifest.jsonagainst a schema and ensures its content (file paths, features) matches the actual files. - Markdown Table Check: Validates that the main
README.mdtable is consistent with the manifests. - PlusCal Translation: Translates any PlusCal code to TLA⁺ to verify syntax.
- Parsing: Uses the SANY parser to check all
.tlafiles for syntactic and semantic validity. - Model Checking: Runs "small" models (runtime < 30s) to completion with TLC or Apalache, verifying their expected outcomes and state counts.
- Smoke Testing: Runs "large" models for a short duration (5 seconds) to ensure they don't crash immediately.
- Proof Checking: Runs the TLAPS proof manager on any modules containing formal proofs.
This flow is illustrated below.
Sources: DEVELOPING.md:8-28, CONTRIBUTING.md:29-32
Conclusion
The structure of a specification in this repository is designed for clarity, maintainability, and automated verification. By combining formal .tla definitions, .cfg model configurations, manifest.json metadata, and README.md documentation, each specification provides a robust and self-contained artifact. This anatomy not only makes the algorithms easier to understand and verify but also creates a valuable, high-quality corpus for the development and testing of TLA⁺ tools.
Sources: README.md:5-11, CONTRIBUTING.md:3-7