# TLA+-Bench: An Execution-Grounded Benchmark and Dataset for Natural-Language to TLA Specification Generation

arXiv: https://arxiv.org/abs/2607.23425 · HTML: https://mlsanity.com/paper/2607.23425/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 18 of its 32 references that are in the map.
- First posted on arXiv 26 Jul 2026.

## Builds on (most cited first, 18 of 18)

- [The Llama 3 Herd of Models](https://mlsanity.com/paper/2407.21783/) (2024)
- [Gemini 2.5: Pushing the Frontier with Advanced Reasoning, Multimodality, Long Context, and Next Generation Agentic Capabilities](https://mlsanity.com/paper/2507.06261/) (2025)
- [SWE-bench: Can Language Models Resolve Real-World GitHub Issues?](https://mlsanity.com/paper/2310.06770/) (2023)
- [LiveCodeBench: Holistic and Contamination Free Evaluation of Large Language Models for Code](https://mlsanity.com/paper/2403.07974/) (2024)
- [Is Your Code Generated by ChatGPT Really Correct? Rigorous Evaluation of Large Language Models for Code Generation](https://mlsanity.com/paper/2305.01210/) (2023)
- [Qwen2.5-Coder Technical Report](https://mlsanity.com/paper/2409.12186/) (2024)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [LiveBench: A Challenging, Contamination-Limited LLM Benchmark](https://mlsanity.com/paper/2406.19314/) (2024)
- [ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics](https://mlsanity.com/paper/2302.12433/) (2023)
- [A Careful Examination of Large Language Model Performance on Grade School Arithmetic](https://mlsanity.com/paper/2405.00332/) (2024)
- [Clover: Closed-Loop Verifiable Code Generation](https://mlsanity.com/paper/2310.17807/) (2023)
- [DafnyBench: A Benchmark for Formal Software Verification](https://mlsanity.com/paper/2406.08467/) (2024)
- [NL2SQL-BUGs: A Benchmark for Detecting Semantic Errors in NL2SQL Translation](https://mlsanity.com/paper/2503.11984/) (2025)
- [VarBench: Robust Language Model Benchmarking Through Dynamic Variable Perturbation](https://mlsanity.com/paper/2406.17681/) (2024)
- [Evaluating the Ability of Large Language Models to Generate Verifiable Specifications in VeriFast](https://mlsanity.com/paper/2411.02318/) (2024)
- [When Names Disappear: Revealing What LLMs Actually Understand About Code](https://mlsanity.com/paper/2510.03178/) (2025)
- [OpenClassGen: A Large-Scale Corpus of Real-World Python Classes for LLM Research](https://mlsanity.com/paper/2504.15564/) (2025)
- [Can LLMs Write Correct TLA+ Specifications? Evaluating Natural-Language-to-TLA+ Generation](https://mlsanity.com/paper/2606.05792/) (2026)

## Abstract (arXiv)

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. We present TLA+-Bench, a dataset and benchmark that grades by execution. Every gold specification ships a configuration the TLA+ model checker runs over the full reachable state space, deciding exactly whether the specification holds the properties that configuration names. The dataset holds 403 model-checked gold and 897 parse-only silver specifications from 13 public repositories, subsumes prior TLA+ generation data, and carries four model-written descriptions in two styles from two providers, with difficulty and category labels. Our main finding is about measurement itself: an exact oracle gives not one correctness number but a range. Varying only the grading choices earlier benchmarks leave unstated, on one fixed set of model outputs, the correct rate moves sixfold, from 10.0% to 1.7%; adding the interface-supply choice, where the model is told the configuration's names, widens the range to elevenfold, from 18.7% to 1.7%. We call this range the correctness envelope and measure each of its bounds. The findings inside it are stable. Every model writes valid TLA+ far more often than correct TLA+: the strongest is correct 16% of the time by default and 26% when given the interface names, open models at most 1%, and correctness falls sharply with difficulty.