TLA-Prover: Verifiable TLA+ Specification Synthesis via Preference-Optimized Low-Rank Adaptation
Published in Proceedings of the 21st International Conference on Software Technologies, 2026
TLA+ is a formal specification language for verifying distributed systems and safety-critical protocols. Large language models (LLMs) frequently produce TLA+ specifications that fail the TLC model checker for semantic reasons. Across 25 LLMs, the best public baseline is 26.6% syntactic parse and 8.6% semantic model-check. We present TLA-Prover, a 20-billion-parameter model for TLA+ specification synthesis. Training combines supervised fine-tuning (SFT) on verified examples with repair-based group-relative policy optimization (GRPO).
Recommended citation: Spencer, E., Bisharat, A., Ortiz, B., Nazari, M., Bhadauria, K., Wang, T., Thiruvathukal, G. K., Läufer, K. and Abuhamad, M. (2026). TLA-Prover: Verifiable TLA+ Specification Synthesis via Preference-Optimized Low-Rank Adaptation. In Proceedings of the 21st International Conference on Software Technologies - ICSOFT; ISBN 978-989-758-855-6; ISSN 2184-2833, SciTePress, pages 627-636. DOI: 10.5220/0015234600004088
Recommended citation: Spencer, E., Bisharat, A., Ortiz, B., Nazari, M., Bhadauria, K., Wang, T., Thiruvathukal, G. K., Läufer, K. and Abuhamad, M. (2026). TLA-Prover: Verifiable TLA+ Specification Synthesis via Preference-Optimized Low-Rank Adaptation. In Proceedings of the 21st International Conference on Software Technologies - ICSOFT; ISBN 978-989-758-855-6; ISSN 2184-2833, SciTePress, pages 627-636. DOI: 10.5220/0015234600004088
Download Paper