Can LLMs Write Correct TLA+ Specifications? Evaluating Natural-Language-to-TLA+ Generation 事件

Can LLMs Write Correct TLA+ Specifications? Evaluating Natural-Language-to-TLA+ Generation 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 th