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.

翻译：TLA+已在亚马逊和微软等公司支撑了工业级形式化验证实践，然而从自然语言编写正确的TLA+形式规约仍需专业知识和大量时间，这限制了其普及应用。大型语言模型（LLM）展现出潜力，但尚无研究系统评估其能否从自然语言生成语义正确的TLA+形式规约。本文首次系统评估了基于LLM的自然语言到TLA+形式规约的合成能力。我们基于包含205个TLA+形式规约的精选数据集，对来自8个系列的30个LLM进行了评估：在四种提示策略下测试了25个开源权重模型（共2600次运行），并在少样本提示条件下评估了5个闭源模型（共130次运行），所有结果均通过SANY语法解析器和TLC模型检查器验证。实验发现LLM的最高语法正确率达26.6%，但语义正确率仅为8.6%，且成功案例全部集中于渐进式提示策略。结果表明模型规模并非质量预测指标——例如DeepSeek r1:8B在所有策略上的表现均优于其70B变体，这暗示了推理对齐能力对形式语言理解的关键作用。代码专用模型因主流编程语言训练导致的负迁移而持续表现不佳。我们识别出五类反复出现的幻觉模式，且均可追溯至特定训练数据偏差。这些结果表明，若无专家监督，当前LLM无法生成可靠的TLA+形式规约。为促进研究可复现性，我们开源了评价框架、代码和数据集。