形式化验证团队终于有了LLM能力的基准数据——当前模型无法可靠生成TLA+规范，但渐进式提示和推理对齐是突破口，做形式化方法或分布式系统验证的开发者值得关注。
TLA+是亚马逊、微软等公司用于工业验证的形式化语言，但将自然语言转化为正确的TLA+规范仍需专家经验。本文首次系统评估了30个LLM（含8个模型家族）在205个TLA+规范上的表现，使用SANY解析器和TLC模型检查器验证。结果显示，LLM最高语法正确率26.6%，但语义正确率仅8.6%，且成功案例全部来自渐进式提示。模型大小与质量无关，例如DeepSeek r1:8b在所有策略上优于其70B版本，表明推理对齐对形式语言更重要。代码专用模型因主流语言训练的负迁移而表现更差。研究识别了五种幻觉类别，均与训练数据偏差有关。
Can LLMs Write Correct TLA+ Specifications? Evaluating Natural-Language-to-TLA+ Generation
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.