Research Updates#
May 11, 2026 - 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).
April 30, 2026 - 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.
April 17, 2026 - 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.
April 11, 2026 - 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.
March 29, 2026 - 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.
August 15, 2025 - 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.
May 08, 2025 - 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.
February 05, 2025 - 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.