Pinned TLAPM and TLA+ tools

Unmodified upstream verification assets preserved for reproducible TLAPS-Bench installation.

TLAPM for Linux x86-64

• Upstream build: 7824dab55e0c346e913404d59d0bbdeebce73cc1.
• Original release: tlaplus/tlapm / 1.6.0-pre.
• Filename: tlapm-1.6.0-pre-x86_64-linux-gnu.tar.gz.
• SHA-256: a2860384bc89c4c5b2c73ec367e29f44d829e4d4a2698ab295139f829219331c.

TLA+ tools / SANY

• Build revision from the jar manifest: 8f4bc8b73ad1202774a6bf70143436f8ba50aab0.
• Original release: tlaplus/tlaplus / v1.8.0.
• Filename: tla2tools.jar.
• SHA-256: ab4694601923fd5ac06452abbf847c366a5054a3d739552085edd6ed986c29ec.

Both files are byte-for-byte identical to the artifacts already locked by TLAPS-Bench. Upstream licenses and notices remain included. The fixed mirrors preserve the existing verifier and parser after their upstream release assets were replaced.

This is a toolchain artifact release, not a TLAPS-Bench version release.

TLAPS-Bench v2.0.0: Proof from Scratch on Complex Protocols and Systems

TLAPS-Bench 2.0 introduces a Current dataset of 9 specifications and 56 proof targets drawn from complex protocols and systems. The challenge is to construct complete, mechanically checked TLA+ proofs from scratch: agents must discover the proof structure, introduce helper definitions and lemmas, and establish the required safety and liveness properties.

This is the new benchmark focus. Proof Completion, the stable scope of v1.0.0, remains available for historical evaluations; the Current dataset measures the harder problem of building proofs without a supplied proof decomposition.

The Current dataset

Problem	Type	Specifications	Proof targets
FLASH cache coherence	Protocol	1	15
ZooKeeper protocol	Protocol	1	9
Cahill's serializable snapshot isolation	Protocol	1	1
Ivy TLB	System	1	2
OpenAddressing	System	1	5
etcd Raft	System	1	8
HashiCorp Raft	System	1	6
ZooKeeper implementation	System	1	9
MongoDB distributed transactions	System	1	1
Total		9	56

The set spans cache coherence, consensus and replication, address translation, concurrent data structures, and transaction isolation. Each specification runs as one module task, allowing agents to share helper lemmas across its proof targets. Scoring retains credit for individual targets whose proofs and dependencies have been verified.

tlaps-bench run now selects this Current dataset by default. The versioned problem-set definition distinguishes current, retired, and next. Retired problems remain in the repository for studying proofs and reproducing historical work. See the leaderboard for reported results and their recorded evaluation revisions.

New features since v1.0.0

• Module-level proof construction. One run tackles a specification's selected targets together, with editable helper and proof regions and a fixed model context.
• Partial credit backed by verified dependencies. The primary Proof-from-Scratch score is trusted proof targets divided by applicable targets (k/n). Targets that rely on unproved lemmas receive no credit. Whole-specification completion and results with continuations are reported separately.
• Explicit dataset selection. Choose current, retired, or next with --task-list, supply an exact task-list file, or search the full corpus with --filter. --dry-run previews the selection without starting containers or calling a model.
• Stronger proof integrity checks. Manifest-defined context, mandatory SANY parsing, fixed statement checks, and grading from clean canonical inputs protect the meaning of the task and reject unsupported proof admissions or context changes.
• Official proof libraries and proof-development tools. Agents can import approved TLAPS and Community Modules proof libraries, use shared proof guidance and task-audit skills, and investigate candidate invariants with Apalache and TLC. Library sources and the TLAPM/SANY verification artifacts are pinned and checked against content hashes.
• Durable verification and resume. Module checkpoints preserve verification progress. Resume validates the recorded task set, inputs, toolchain, and execution settings. Verification budgets scale with the module's target count and enforce CPU limits.
• Expanded backend options. Cursor joins the existing agentic integrations. Optional reasoning-effort controls and additional one-shot Proof Completion backends support different evaluation settings; Proof from Scratch requires a tool-using backend.
• Richer evaluation records. Reports include token usage, tool-call counts, separate agent and grading time, and equivalent cost where available. Infrastructure failures and quota interruptions are distinguished from scored proof failures.

Run the Current dataset

Install uv and Docker, then clone the release:

git clone --branch v2.0.0 --depth 1 https://github.com/specula-org/TLAPS-Bench.git
cd TLAPS-Bench
uv run --locked tlaps-bench run --dry-run
uv run --locked tlaps-bench run --jobs 1

The preview lists 9 specifications and 56 proof units. Configure credentials for your chosen backend before the proof run; the default backend is Codex. The first proof run builds the sandbox image. See the usage guide for authentication, backend selection, and hardware guidance. Large proofs can require substantial memory, so start with one job.

For a small example outside Current:

uv run --locked tlaps-bench run --filter Euclid/Euclid-Hyperbook/GCD.tla --jobs 1

Changes for existing users

• The default mode changes from proof-completion to proof-from-scratch, and an unfiltered run selects Current. Use --mode proof-completion explicitly for Proof Completion.
• Proof-from-Scratch runs use benchmark/proof-from-scratch-module/. The theorem-level benchmark/proof-from-scratch/ tree is the generator's target-selection input.
• Dataset contents, task boundaries, and grading differ from v1.0.0. Keep the original checkout and recorded run settings for historical results; old theorem-level runs cannot be resumed as module runs. Report the benchmark revision with scores and compare runs on the same task set and evaluation settings.

The project remains MIT-licensed. Third-party sources and licenses are documented in NOTICE and LICENSES.

TLAPS Bench v1.0.0: Proof Completion

v1.0.0 is the first stable release of the TLAPS Proof Benchmark's proof-completion dataset and evaluation workflow.

This release establishes a versioned benchmark baseline of 483 proof-completion tasks across 55 examples. Each task presents a TLA+ theorem with its target proof replaced by PROOF OBVIOUS, a solution passes only when it is accepted by TLAPS and satisfies the benchmark's integrity checks.

Release scope

The stable dataset, validation, and compatibility scope of v1.0.0 covers proof-completion only.

The repository also contains the developing proof-from-scratch mode. It is included as an experimental preview and is not part of the v1.0.0 benchmark contract or stability guarantees.

Contents

• 483 proof-completion tasks collected from established TLA+ and TLAPS example libraries and systems specifications.
• A unified tlaps-bench CLI for running, checking, validating, generating, and scoring benchmark tasks.
• Integrity checks that reject modifications outside the permitted target proof and detect admitted or otherwise invalid solutions.
• Containerized execution with a bundled proof-checking toolchain, plus a native execution option for supported development environments.
• Parallel execution, resumable runs, structured result files, and summary reports for evaluation campaigns.

Quick start

git clone --branch v1.0.0 --depth 1 https://github.com/specula-org/tlaps-bench.git
cd tlaps-bench
uv run --locked tlaps-bench run --mode proof-completion --filter GCD_GCD3

See the usage guide
for setup, backend configuration, and full benchmark runs.

Dataset and licensing

The per-example dataset breakdown is available in docs/DATASET.md.

The project is released under the MIT License. Third-party benchmark sources and their applicable licenses are documented in NOTICE and LICENSES/.