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/.