Posts tagged TLA+

TLA-Prover Paper Accepted to ICSOFT 2026

We are pleased to announce that our latest research paper, “TLA-Prover: Verifiable TLA+ Specification Synthesis via Preference-Optimized Low-Rank Adaptation” (Paper #131), has been accepted for publication at ICSOFT 2026 (International Conference on Software Technologies) in Porto, Portugal.

Read more ...

New Paper: TLA-Prover — Fine-Tuning LLMs for Verifiable TLA+ Specification Synthesis

Building on our evaluation study that showed the best public LLMs achieve only 8.6% semantic correctness on TLA+ specification generation, we present TLA-Prover: a 20-billion-parameter model trained specifically for TLA+ specification synthesis.

Read more ...

Presented Two Posters at GCASR 2026

On May 11, 2026 we presented two posters at the 13th Greater Chicago Area Systems Research Workshop (GCASR 2026).

Read more ...

Our Paper on LLM-Based TLA+ Specification Generation Has Been Accepted

We are excited to announce that our paper Can LLMs Write Correct TLA+ Specifications? Evaluating Natural-Language-to-TLA+ Generation has been accepted for publication at ICSOFT 2026 (International Conference on Software Technologies) in Porto, Portugal.

Read more ...

Interactive Microwave: TLA+ in the Browser

We published a browser-native version of the interactive-microwave-tla simulator. It mimics a Java microwave runtime and a small TLA+ model checker that is a literal transcription of the project’s Microwave.tla spec, so students can experiment with the state machine — including the stuttering liveness failure from Laufer, Mertin, and Thiruvathukal, arXiv:2407.21152 — without installing Java, Maven, or TLC.

Read more ...

Eric Spencer Presents ChatTLA+ at Loyola University Chicago

Eric Spencer presented ChatTLA+ at the Undergraduate Research and Engagement Symposium at Loyola University Chicago on April 17, 2026 - a talk exploring the use of large language models for generating and verifying TLA+ formal specifications.

Read more ...

Brian Ortiz Presents Poster at Graduate School Interdisciplinary Research Symposium 2026

Brian Ortiz presented a poster at the Graduate School Interdisciplinary Research Symposium (GSIRS 2026) on April 11, 2026, at Loyola University Chicago.

Read more ...

Can LLMs Write Correct TLA+ Specifications? Our New Evaluation Study

We have submitted a new paper evaluating whether large language models can generate semantically correct TLA+ specifications from natural language. We evaluated 30 LLMs across eight families on 205 TLA+ specifications. Best semantic correctness achieved was only 8.6%, and model size did not predict quality.

Read more ...

Eric Spencer Awarded Mulcahy Scholar Stipend

Eric Spencer, an undergraduate researcher in the AI4FM group, has been awarded a $1,000 Mulcahy Scholar stipend from the Loyola University Chicago College of Arts and Sciences to support his research on LLM-based TLA+ specification synthesis.

Read more ...

Brian Ortiz Presents Poster at GCASR 2025

Brian Ortiz presented a work-in-progress poster at the 12th Greater Chicago Area Systems Research Workshop (GCASR 2025), held on May 8, 2025 at Loyola University Chicago’s Water Tower Campus.

Read more ...

TLA+ for All: Running Model Checking in a Python Notebook

We published a project embedding TLA+ model checking directly into a Python notebook environment, making formal verification accessible without any installation. Users can write specifications, run the TLC model checker, and visualize behaviors in-browser.

Read more ...