Benchmark RadarTLA+-Bench
TLA+-Bench evaluates natural-language to TLA+ specification generation by executing each specification in the TLA+ model checker across the full reachable state space. The dataset includes 403 model-checked gold and 897 parse-only silver specifications, with multiple descriptions and difficulty labels.
- Released
- 2026-07-26
- Readiness
- Paper only
- Primary field
- General AI
Why it matters
Prior benchmarks for formal specification generation grade by reference resemblance or parseability, not correctness. TLA+-Bench provides an execution-grounded oracle that measures whether generated specifications satisfy the required properties, offering a more reliable evaluation signal and revealing a range of correctness scores depending on grading choices.
Motivation
Large language models increasingly write TLA$^{+}$ formal specifications from natural-language descriptions, but progress is hard to measure: existing resources grade by resemblance to a reference or by whether the output parses, neither of which shows correctness.
Primary resources
Benchmark Radar records only publicly supported details and links back to primary sources for verification.