Symbolic Model Checking with Apalache
Relevant source files
The following files were used as context for generating this wiki page:The TLA+ Examples repository utilizes a diverse set of verification tools to check the correctness of its specifications. Alongside the explicit-state model checker TLC and the proof system TLAPS, the repository uses Apalache for symbolic model checking. Apalache is particularly suited for certain classes of specifications and provides an alternative verification method within the project's ecosystem.
This document outlines the role of Apalache in the repository, how to contribute specifications that use it, and how these specifications are validated through the project's continuous integration (CI) pipeline. The use of different tools like Apalache, TLC, and TLAPS allows the repository to serve as a comprehensive library for demonstrating various formal verification techniques.
Sources: README.md:6-16
Verification Tooling Overview
The repository employs three primary tools for verifying TLA+ specifications. Each tool serves a different purpose, and specifications are tagged to indicate which tool(s) can be used for their verification.
This diagram shows the three main verification tools used in the repository for checking TLA+ specifications.
Sources: README.md:14-16
Identifying Apalache Specifications
Specifications intended to be checked with Apalache are identified through metadata in their directory's manifest.json file. A model is designated for symbolic checking if its mode is set to "symbolic". Additionally, the main README.md file contains a table that explicitly flags which specifications support Apalache.
The following specifications are listed as using Apalache for verification:
| Name | Author(s) |
|---|---|
| Einstein's Riddle | Isaac DeFrain, Giuliano Losa |
| Termination | Giuliano Losa |
| Raft (with cluster changes) | George Pîrlea, Darius Foom, Brandon Amos, Huanchen Zhang, Daniel Ricketts |
Sources: README.md:88-89, 211, 220, CONTRIBUTING.md:78-81
Contributing an Apalache Specification
Contributors wishing to add a TLA+ specification that is checked with Apalache must follow a specific process to ensure it is correctly integrated into the project and its CI system.
The process involves creating a manifest.json file and correctly configuring the model for symbolic checking.
This flowchart illustrates the steps for contributing a specification that will be checked by Apalache.
Sources: CONTRIBUTING.md:29-50, 78-81, 98-112
Manifest Configuration
The manifest.json file is crucial for CI integration. For a model to be recognized as an Apalache model, its configuration must be set accordingly.
The key field is mode, which must be set to "symbolic".
| Field | Type | Description | Example |
|---|---|---|---|
path | string | Path to the model's .cfg file. | specifications/MySpec/MyModel.cfg |
runtime | string | Approximate runtime ("HH:MM:SS"). | "00:00:25" |
mode | string | The checking mode. Must be "symbolic" for Apalache. | "symbolic" |
result | string | The expected outcome of the check (e.g., "success", "safety failure"). | "success" |
Sources: CONTRIBUTING.md:72-81
Below is an example snippet from a manifest.json file for a model intended for Apalache:
{
"path": "specifications/MySpec/MyModel.cfg",
"runtime": "00:00:25",
"mode": "symbolic",
"result": "success"
}
Sources: CONTRIBUTING.md:72-81
Continuous Integration (CI) Validation
All specifications, including those checked by Apalache, are subject to automated validation in the CI pipeline. This ensures that the examples remain correct and functional over time.
The CI workflow uses several Python scripts to validate manifests, parse modules, and run the appropriate verification tools.
This diagram shows a simplified view of the CI pipeline, highlighting how it dispatches models to Apalache based on their configuration.
Sources: DEVELOPING.md:8-25
CI Scripts for Apalache
Two main scripts are responsible for executing Apalache checks:
check_small_models.py: This script runs Apalache to completion on all models marked as "small" (runtime under 30 seconds). It verifies that the model check completes with theresultspecified in themanifest.json(e.g., success or a specific failure type) and does not crash.smoke_test_large_models.py: For models that take longer than 30 seconds, this script runs Apalache for a short duration (five seconds) to ensure they initialize correctly and do not crash immediately. This acts as a basic "smoke test".
These scripts ensure that all Apalache-based examples in the repository are continuously validated.
Sources: DEVELOPING.md:21-28
Summary
Apalache is an integral part of the verification toolkit for the TLA+ Examples repository, providing symbolic model checking capabilities. Its integration is managed through manifest.json metadata, which allows the CI pipeline to automatically identify and run Apalache on relevant specifications. This structured approach ensures that contributed Apalache examples are consistently validated, maintaining the high quality and reliability of the repository as a key resource for the TLA+ community.
Sources: README.md:6-16, CONTRIBUTING.md:14-17, DEVELOPING.md:41-45