Posts by Collection

Portfolio item number 1

Short description of portfolio item number 1

Portfolio item number 2

Short description of portfolio item number 2

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

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+-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

Talk 1 on Relevant Topic in Your Field

Published: March 01, 2012

This is a description of your talk, which is a markdown file that can be all markdown-ified like any other post. Yay markdown!

Tutorial 1 on Relevant Topic in Your Field

Published: March 01, 2013

More information here

Talk 2 on Relevant Topic in Your Field

Published: February 01, 2014

More information here

Conference Proceeding talk 3 on Relevant Topic in Your Field

Published: March 01, 2014

This is a description of your conference proceedings talk, note the different field in type. You can put anything in this field.

Teaching experience 1

Undergraduate course, University 1, Department, 2014

This is a description of a teaching experience. You can use markdown like any other post.

Teaching experience 2

Workshop, University 1, Department, 2015

This is a description of a teaching experience. You can use markdown like any other post.