Posts tagged TLA+
Presented Two Posters at GCASR 2026
- 11 May 2026
On May 11, 2026 we presented two posters at the 13th Greater Chicago Area Systems Research Workshop (GCASR 2026).
Our Paper on LLM-Based TLA+ Specification Generation Has Been Accepted
- 30 April 2026
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.
Eric Spencer Presents ChatTLA+ at Loyola University Chicago
- 17 April 2026
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.
Brian Ortiz Presents Poster at Graduate School Interdisciplinary Research Symposium 2026
- 11 April 2026
Brian Ortiz presented a poster at the Graduate School Interdisciplinary Research Symposium (GSIRS 2026) on April 11, 2026, at Loyola University Chicago.
Can LLMs Write Correct TLA+ Specifications? Our New Evaluation Study
- 29 March 2026
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.
Eric Spencer Awarded Mulcahy Scholar Stipend
- 15 August 2025
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.
Brian Ortiz Presents Poster at GCASR 2025
- 08 May 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.
TLA+ for All: Running Model Checking in a Python Notebook
- 05 February 2025
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.