Publications

Journal Articles

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

Published in Proceedings of the 21st International Conference on Software Technologies, 2026

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.

Recommended citation: Bisharat, A., Ortiz, B., Spencer, E., Bhadauria, K., Wang, T., Thiruvathukal, G. K., Läufer, K. and Abuhamad, M. (2026). Can LLMs Write Correct TLA + Specifications? Evaluating Natural-Language-to-TLA + Generation. In Proceedings of the 21st International Conference on Software Technologies - ICSOFT; ISBN 978-989-758-855-6; ISSN 2184-2833, SciTePress, pages 39-50. DOI: 10.5220/0015070400004088
Download Paper

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
Download Paper

Working Papers

TLA+-Bench: An Execution-Grounded Benchmark and Dataset for Natural-Language to TLA+ Specification Generation

Published in arXiv, 2026

Large language models increasingly write TLA+ formal specifications from natural-language descriptions, but progress is hard to measure: existing resources grade by resemblance to a reference or by whether the output parses, neither of which shows correctness. We present TLA+-Bench, a dataset and benchmark that grades by execution. Every gold specification ships a configuration the TLA+ model checker runs over the full reachable state space, deciding exactly whether the specification holds the properties that configuration names. The dataset holds 403 model-checked gold and 897 parse-only silver specifications from 13 public repositories, subsumes prior TLA+ generation data, and carries four model-written descriptions in two styles from two providers, with difficulty and category labels.

Recommended citation: Bisharat, A., Spencer, E., Ortiz, B., Bhadauria, K., Nazari, M., Santos, B., Ramos, A., Wang, T., Thiruvathukal, G.K., Läufer, K. and Abuhamad, M. (2026) TLA+-Bench: An Execution-Grounded Benchmark and Dataset for Natural-Language to TLA+ Specification Generation. arXiv:2607.23425. Available at: https://arxiv.org/abs/2607.23425.
Download Paper