3 papers
cs.SE2026
TLA+-Bench: An Execution-Grounded Benchmark and Dataset for Natural-Language to TLA Specification Generation
Arslan Bisharat, Eric Spencer, Brian Ortiz +8
Large language models increasingly write TLA formal specifications from natural-language descriptions, but progress is hard to measure: existing resources grade by resemblanc…
cs.SE2026
TLA-Prover: Verifiable TLA+ Specification Synthesis via Preference-Optimized Low-Rank Adaptation
Eric Spencer, Arslan Bisharat, Brian Ortiz +6
TLA+ is a formal specification language for verifying distributed systems and safety-critical protocols. Large language models (LLMs) frequently produce TLA+ specifications that fa…
cs.AI2026
Can LLMs Write Correct TLA+ Specifications? Evaluating Natural-Language-to-TLA+ Generation
Arslan Bisharat, Brian Ortiz, Eric Spencer +5
TLA+ has supported industrial verification at companies such as Amazon and Microsoft, yet writing correct TLA+ specifications from natural language still requires time and expertis…