Proving Correctness with TLAPS
Relevant source files
The following files were used as context for generating this wiki page:The TLA⁺ Examples repository utilizes the TLA⁺ Proof System (TLAPS) to formally verify the correctness of various algorithms and specifications. While many specifications are validated using the TLC model checker, a significant number also include machine-checked proofs, providing a higher degree of assurance. These proofs are an integral part of the repository, demonstrating how to formally prove properties of TLA⁺ specifications.
This document outlines how proofs are structured, validated, and used within the repository, based on the provided specifications and project documentation. The focus is on the role of TLAPS in ensuring algorithmic correctness through rigorous, hierarchical proofs that are automatically verified by the project's continuous integration (CI) system.
Sources: README.md, DEVELOPING.md
Identifying and Contributing Proofs
Specifications that include formal proofs are clearly marked within the repository. The main README.md file contains a table of all validated examples, with a "TLAPS Proof" column indicating which specs contain proofs.
Sources: README.md:29-32
Manifest Metadata
Each specification directory contains a manifest.json file that holds metadata about the TLA⁺ modules and models. For modules containing proofs, a proof object is included, which specifies the approximate runtime required to check the proof with TLAPM (the TLA+ Proof Manager).
{
"path": "specifications/LoopInvariance/BinarySearch.tla",
"features": [
"pluscal"
],
"models": [],
"proof": {
"runtime": "00:00:01"
}
}
Source: specifications/LoopInvariance/manifest.json:15-24
This metadata is crucial for the CI system to determine how to handle the proof verification.
Contribution Workflow
When contributing a new specification with a proof, developers must update the manifest.json file to include the proof's runtime. This ensures the proof is integrated into the automated validation process.
The following diagram illustrates the workflow for contributing a spec with a TLAPS proof.
This diagram shows the process for adding a new specification with a formal proof to the repository.
Sources: CONTRIBUTING.md:49-60
CI Validation of Proofs
The integrity of the proofs is maintained through automated CI checks. The CI pipeline includes a dedicated script, check_proofs.py, which executes the TLA+ Proof Manager (TLAPM) against all modules that declare a proof in their manifest.json.
- Execution: The script runs TLAPM on all modules containing formal proofs to ensure they remain valid.
- Runtime Condition: Proofs with a recorded runtime of less than one minute are checked in their entirety during the CI run. Longer-running proofs may be handled differently or checked less frequently.
This automated validation ensures that proofs do not become outdated or incorrect as the TLA⁺ language and tools evolve.
Sources: DEVELOPING.md:26-27, CONTRIBUTING.md:58-59
Proof Examples
The repository contains a diverse set of specifications with TLAPS proofs, ranging from beginner-friendly examples to complex refinement proofs of distributed algorithms.
Table of Proof Examples
| Specification Name | Author(s) | Description | Proof Runtime |
|---|---|---|---|
Learn TLA⁺ Proofs | Andrew Helwer | A beginner-friendly introduction to writing TLA⁺ proofs. | 00:00:10 |
Loop Invariance | Leslie Lamport | Proves partial correctness of sequential algorithms like BinarySearch and Quicksort. | 00:00:01 |
Peterson Lock Refinement | Jarod Differdange | A two-way refinement proof between Peterson's algorithm and an abstract lock. | Not specified |
EWD998 | Stephan Merz, Markus Kuppe | Proves refinement between different termination detection algorithms. | Not specified |
Boyer-Moore Majority Vote | Stephan Merz | Proves correctness of the majority vote algorithm. | 00:00:01 |
Sources: README.md:35-60, specifications/LearnProofs/manifest.json, specifications/LoopInvariance/manifest.json
Loop Invariance Proofs
The LoopInvariance examples demonstrate how to prove the partial correctness of simple sequential algorithms. This is achieved by defining a loop invariant, named Inv in the specifications, and then formally proving that this invariant is maintained throughout the algorithm's execution.
The directory includes TLAPS-checked proofs for:
SumSequenceBinarySearchQuicksort(partly checked, partly informal)
These examples serve as practical exercises for understanding how to find and prove loop invariants.
Sources: specifications/LoopInvariance/README.txt
Refinement Proofs
TLAPS is also used to prove refinement, which shows that all behaviors of a concrete implementation are valid behaviors of a more abstract specification.
Peterson's Lock with Auxiliary Variables
The locks_auxiliary_vars specification provides an example of a two-way refinement proof.
Peterson.tla: Proves that Peterson's algorithm refines an abstract lock specification (Lock!Spec).LockHS.tla: Proves that an abstract lock extended with auxiliary variables (a history variableh_turnand a stuttering variables) refines Peterson's algorithm. This demonstrates a less common but powerful technique for proving refinement from an abstract spec to a concrete one.
Sources: specifications/locks_auxiliary_vars/README.md:3-25
EWD998 Refinement Hierarchy
The ewd998 specification for termination detection is part of a larger refinement hierarchy. TLAPS is used to prove that AsyncTerminationDetection correctly refines SyncTerminationDetection. This chain of refinements connects a high-level abstraction to a more detailed implementation.
The following diagram shows the refinement relationships between the different modules.
This diagram illustrates the refinement hierarchy for the EWD998 termination detection algorithm.
Conclusion
The use of TLAPS for formal proofs is a cornerstone of the TLA⁺ Examples repository's approach to quality and correctness. By providing a rich set of machine-checked proofs and integrating their validation into the CI pipeline, the project not only offers valuable learning resources but also ensures a high standard of reliability for the included algorithmic specifications. These proofs cover a range of concepts, from basic loop invariants to complex refinement hierarchies, making them an essential tool for both learning TLA⁺ and developing verifiably correct systems.