Publications

Papers, talks, and tools from the AI4FM / FMitF group at Loyola University Chicago, under Prof. Konstantin Läufer.

I work on generating TLA+ specifications with language models and checking what those models actually get right. The papers below cover evaluation, training with model-checker feedback, and the datasets needed to reproduce the results. For runnable examples, see my TLA+ projects and tools.

Papers

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

Arslan Bisharat, Eric Spencer, Brian Ortiz, Khushboo Bhadauria, Mujtaba Nazari, Beatriz Santos, Anisa Ramos, TaiNing Wang, George K. Thiruvathukal, Konstantin Läufer, Mohammed Abuhamad.

2026 · arXiv preprint, arXiv:2607.23425 · Coauthor. DOI: 10.48550/arXiv.2607.23425

We built a benchmark that checks generated specifications by running them. It contains 403 model-checked specifications and 897 parse-only specifications from 13 public repositories. On a fixed set of model outputs, changing the grading rules moves the measured correctness rate from 10.0% to 1.7%. The paper makes those choices explicit so that a reported score says what was actually checked.

Paper on arXiv · Dataset, grader & model outputs

TLA-Prover: Verifiable TLA+ Specification Synthesis via Preference-Optimized Low-Rank Adaptation

Eric Spencer, Arslan Bisharat, Brian Ortiz, Mujtaba Nazari, Khushboo Bhadauria, TaiNing Wang, George K. Thiruvathukal, Konstantin Läufer, Mohammed Abuhamad.

2026 · ICSOFT 2026, pp. 627–636 · First author. DOI: 10.5220/0015234600004088

We trained a 20-billion-parameter model to generate TLA+ specifications, using supervised fine-tuning followed by repair-based reinforcement learning with TLC feedback. The paper reports 9 of 30 held-out problems passing both model checking and the Diamond check, which tests whether an altered invariant produces a violation. These are results for the paper's benchmark and evaluation procedure; they do not establish correctness on arbitrary systems.

Published paper · Preprint · Training code · ChatTLA model · Training data & benchmark notes

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

Arslan Bisharat, Brian Ortiz, Eric Spencer, Khushboo Bhadauria, TaiNing Wang, George K. Thiruvathukal, Konstantin Läufer, Mohammed Abuhamad.

2026 · ICSOFT 2026, pp. 39–50 · Coauthor. DOI: 10.5220/0015070400004088

We evaluated 30 language models against a corpus of 205 TLA+ specifications, checking their output with SANY and TLC. The study found a substantial gap between producing valid syntax and satisfying the modeled properties: the best reported rates were 26.6% and 8.6%, respectively. Larger models did not consistently do better. This evaluation motivated the later work on verifier feedback during training.

Published paper · Preprint · FormaLLM code & corpus

Presentations & Posters

2026-04-17Presented ChatTLA+ at Loyola's Undergraduate Research & Engagement Symposium. [link] [eCommons]

2026-04-11Co-author on the GSIRS 2026 poster about systematic evaluation of LLM→TLA+ synthesis. [link]

Models & Datasets

2026chattla-20b model and model card — the ChatTLA model release on Hugging Face. See the card for checkpoint details and the TLA-Prover paper for its reported evaluation.

2026ChatTLA+ training corpus and benchmark — an explanation of the 209-row SFT corpus and 30-problem benchmark. The dataset repository retains its review-era anonymized name.

2026TLA+-Bench dataset and reproduction code — the separate 1,300-specification release used in TLA+-Bench.

Tools

2026FormaLLM — toolkit for evaluating LLMs on formal-specification synthesis. [repo]

2025TLA-Extraction — work on extracting TLA+ specifications from research papers. The original repository is not publicly available; the TLA+-Bench release provides a public collection of specifications and their source references.

Awards

2025Awarded the Mulcahy Scholar stipend for LLM-based TLA+ research. [link]

2022Awarded the Presidential Scholarship at Loyola University Chicago.