Skip to content

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

Latest
Latest

Choose a tag to compare

View all tags
@Qian-Cheng-nju Qian-Cheng-nju released this 29 Sep 15:10
v2.0.0
ef53d03
This commit was created on GitHub.com and signed with GitHub’s verified signature.
GPG key ID: B5690EEEBB952194
Verified
Learn about vigilant mode.

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.

Assets 2
Loading