A benchmark for evaluating AI's ability to write TLAPS (TLA+ Proof System) proofs.
Benchmark results are available on the TLAPS-Bench website.
TLAPS proofs are checked mechanically by tlapm: a proof is either accepted or
rejected, with no partial credit and no room for a plausible-but-wrong argument.
That makes proof construction a sharp test of an AI's formal reasoning.
Each task presents a TLA+ theorem whose proof body is replaced by PROOF OBVIOUS;
the AI must replace it with a real proof that tlapm accepts. Tasks come in two
types:
- Proof completion (
--mode proof-completion) — the model and proof scaffold (inductive invariants, lemma decomposition, and preceding lemmas markedPROOF OMITTED) are given as read-only context, and the AI fills in one marked target proof. - Proof from scratch (
--mode proof-from-scratch) — only the model and the target theorem statement remain; the AI must invent the entire proof structure, including any helper lemmas.
The benchmark draws on two kinds of source. A base of classic TLA+ example
libraries, a small set of systems specifications — real
protocols, several with no published proof. Both sets are expected to keep
growing as more specifications are added.
A – marks a source with no human proofs, from which no proof-completion task
can be derived.
Example libraries
| Source | Examples | Proof completion | Proof from scratch | Total |
|---|---|---|---|---|
| tlaplus/Examples | 45 | 369 | 132 | 501 |
| TLAPS distribution examples | 14 | 103 | 57 | 160 |
| Subtotal | 59 | 472 | 189 | 661 |
Systems specifications
| Source | Examples | Proof completion | Proof from scratch | Total |
|---|---|---|---|---|
| ZooKeeper (Remix) | 2 | – | 18 | 18 |
| Ivy liveness | 6 | – | 12 | 12 |
| etcd (Specula) | 1 | – | 8 | 8 |
| OpenAddressing | 1 | 1 | 5 | 6 |
| two_thread_mutex (Anvil) | 1 | – | 1 | 1 |
| Subtotal | 11 | 1 | 44 | 45 |
70 examples, 706 tasks in total. A per-example breakdown is in
docs/DATASET.md.
Requirements: uv and Docker. Windows users should run the benchmark through WSL2; native Windows is not supported.
git clone https://github.com/specula-org/tlaps-bench.git
cd tlaps-bench
export OPENAI_API_KEY=sk-... # This step is optional: Codex is the default backend if no OpenAI key is provided.
uv run tlaps-bench run --filter GCD_GCD3The first run builds a sandbox Docker image (tlapm, SANY, and the proof checker
bundled in) and runs the task inside it — a firewall allows only the LLM API
hosts, and the benchmarks are mounted read-only. Later runs reuse the image.
Results land in results/<mode>/<backend>/<timestamp>/.
Scale up, or switch task type:
# Full proof-completion suite: 10 in parallel, 2h timeout each
uv run tlaps-bench run --jobs 10 --timeout 7200
# Proof from scratch
uv run tlaps-bench run --mode proof-from-scratch --jobs 10Each run writes results.json and summary.md (with the headline pass rate);
uv run tlaps-bench score (re)computes and compares pass rates. Use --resume
with a fixed --output-dir to skip tasks already recorded as PASS, and
--force-build to rebuild the image after changing source.
Choosing an agent (--backend / --model) and its credentials, the full CLI
reference, and native (--no-container) setup are covered in the
usage guide.
MIT — see LICENSE. Third-party benchmark sources are attributed in
NOTICE.