Can LLMs Write Correct TLA+ Specifications? Evaluating Natural-Language-to-TLA+ Generation
Arslan Bisharat, Brian Ortiz, Eric Spencer, Khushboo Bhadauria, TaiNing Wang, George K. Thiruvathukal, Konstantin Laufer, Mohammed Abuhamad
Why It Matters
What makes this one worth your time
Understanding the limitations of LLMs in generating formal specifications is crucial for improving their reliability in industrial applications, particularly in verification tasks.
This study assesses LLMs' capability to generate TLA+ specifications, highlighting significant limitations in correctness.
Summary
The paper systematically evaluates the ability of 30 LLMs to generate correct TLA+ specifications from natural language, revealing low rates of syntactic and semantic correctness and identifying factors influencing performance.
Key contributions
- First systematic evaluation of LLMs for TLA+ specification synthesis from natural language.
- Identification of five categories of hallucinations in generated specifications linked to training data biases.
- Release of an evaluation framework, code, and dataset for reproducibility and future research.
Notable insights
- Model size does not correlate with performance in generating TLA+ specifications, indicating that reasoning alignment is more critical than sheer scale.
- Code-specialized models underperform due to negative transfer, suggesting that training on mainstream language data may hinder performance in formal language tasks.
Possible limitations
- The abstract does not discuss potential variations in LLM performance across different domains or types of specifications.
Abstract
arXiv:2606.05792v1 Announce Type: new Abstract: TLA+ has supported industrial verification at companies such as Amazon and Microsoft, yet writing correct TLA+ specifications from natural language still requires time and expertise, which limits adoption. LLMs show promise, but no prior study measures whether they produce semantically correct TLA+ specifications from natural language. This paper presents the first systematic evaluation of LLM-based TLA+ specification synthesis from natural language. Our study evaluates 30 LLMs across eight families on a curated dataset of 205 TLA+ specifications: 25 open-weight models across four prompting strategies (2,600 runs) and 5 proprietary models under few-shot prompting (130 runs), all validated by the SANY parser and TLC model checker. LLMs achieve up to 26.6% syntactic correctness but only 8.6% semantic correctness, with successes exclusive to progressive prompting. Results show that model size does not predict quality, e.g., DeepSeek r1:8b outperforms its 70B variant across all strategies, which suggests the importance of reasoning alignment for formal languages. Code-specialized models consistently underperform due to negative transfer from mainstream language training. We identify five recurring hallucination categories, all traceable to specific training data biases. These results suggest that current LLMs do not generate reliable TLA+ specifications without expert oversight. We release the evaluation framework, code, and dataset to support reproducibility and future research.