Proof-Oriented Specifications

This repository contains a collection of TLA⁺ specifications that are not only model-checked with TLC but also include formal, machine-checked proofs of correctness using the TLA⁺ Proof System (TLAPS). These specifications serve as valuable case studies and examples for applying formal proof techniques to algorithms, demonstrating a higher level of verification beyond model checking. The proofs typically focus on safety properties, partial correctness, and refinement relationships between different levels of abstraction.

The presence of a formal proof is a key metadata point for specifications in this repository. It is tracked in manifest.json files and validated by the continuous integration (CI) system, ensuring that all proofs remain valid as the specifications evolve. Many of these specifications are marked as beginner-friendly, providing a structured path for learning how to write TLA⁺ proofs.

Sources: README.md:1-12, README.md:20-22

Proof Verification in CI

The project's continuous integration pipeline automatically validates all formal proofs to ensure their correctness. This is managed by a dedicated script that interacts with the TLA⁺ Proof Manager (TLAPM).

Sources: DEVELOPING.md:10-11, DEVELOPING.md:30-31

CI Workflow

The CI process for proofs is triggered for every pull request. The system identifies modules containing proofs by checking the manifest.json file within each specification's directory. If a proof is declared, the check_proofs.py script invokes TLAPM to verify it.

The following diagram illustrates the proof verification flow within the CI pipeline.

Manifest Declaration

To integrate a proof into the CI system, it must be declared in the manifest.json file for the specification. This involves adding a proof object to the corresponding module entry, which includes the approximate runtime. Proofs with a runtime of less than one minute are checked in their entirety by the CI.

Here is an example from the byzpaxos specification:

{
  "path": "specifications/byzpaxos/Consensus.tla",
  "features": ["pluscal"],
  "models": [],
  "proof": {
    "runtime": "00:00:01"
  }
}

This snippet from byzpaxos/manifest.json declares a formal proof for Consensus.tla with a 1-second runtime.

Sources: specifications/byzpaxos/manifest.json:28-39, CONTRIBUTING.md:50-52

Key Proof Techniques and Concepts

The repository showcases several fundamental techniques for structuring formal proofs in TLA⁺.

Loop Invariants

Proving partial correctness of sequential algorithms often relies on identifying a correct loop invariant. The LoopInvariance specification provides simple examples written in PlusCal to demonstrate this concept. The invariants are named Inv within the specifications, and the modules contain complete TLAPS-checked proofs.

Examples include:

• SumSequence
• BinarySearch
• Quicksort (contains a partly checked, partly informal proof)

Users are encouraged to find the invariants and write their own proofs before consulting the provided solutions.

Sources: specifications/LoopInvariance/README.txt:1-14

Refinement and Auxiliary Variables

Refinement is a technique to prove that a detailed, low-level implementation correctly implements a more abstract, high-level specification. The locks_auxiliary_vars specification provides an example of a two-way refinement proof between Peterson's algorithm and an abstract lock.

This is achieved using auxiliary variables:

• History Variables: A history variable h_turn is used to emulate the turn variable of Peterson's algorithm in the abstract lock specification.
• Stuttering Variables: A stuttering variable s is introduced to force stuttering steps, allowing the abstract lock acquisition to match the three steps taken by Peterson's algorithm.

The diagram below shows the refinement relationships demonstrated in this example.

A more complex example of refinement is found in the ewd998 specification for termination detection, which demonstrates a chain of refinements.

Examples of Proof-Oriented Specifications

The repository contains numerous specifications with formal proofs, varying in complexity.

Sources: README.md:20-41, specifications/LearnProofs/manifest.json, specifications/sums_even/manifest.json, specifications/LoopInvariance/README.txt, specifications/byzpaxos/manifest.json, specifications/locks_auxiliary_vars/README.md

Summary

The proof-oriented specifications in this repository are a critical resource for both learning and practical application of formal verification with TLA⁺. They demonstrate how to move beyond model checking to create machine-checked, rigorous proofs of algorithm correctness, safety, and refinement. The integration of TLAPS into the project's CI ensures that these proofs are continuously validated, maintaining a high standard of quality and providing a reliable set of examples for the TLA⁺ community.

Sources: README.md:4-7, CONTRIBUTING.md:3-6