Our Paper on LLM-Based TLA+ Specification Generation Has Been Accepted#
We are excited to announce that our paper Can LLMs Write Correct TLA+ Specifications? Evaluating Natural-Language-to-TLA+ Generation has been accepted for publication at ICSOFT 2026 (International Conference on Software Technologies) in Porto, Portugal.
The paper presents the first systematic evaluation of LLM-based TLA+ specification synthesis from natural language, evaluating 30 LLMs across eight families on a curated dataset of 205 TLA+ specifications. Key findings include that LLMs achieve up to 26.6% syntactic correctness but only 8.6% semantic correctness, and that model size does not predict quality on formal languages.