AI for Formal Methods#
Welcome to AI4FM - the AI for Formal Methods research group at Loyola University Chicago, part of the Department of Computer Science. We advance formal methods, rigorous system design, and reproducible tools at the intersection of AI, logic, mathematics, and real-world computing.
Featured Research#
Can LLMs Write Correct TLA+ Specifications?
Evaluating Natural-Language-to-TLA+ Generation - Accepted at ICSOFT 2026
The first systematic evaluation of LLM-based TLA+ specification synthesis from natural language. We evaluate 30 LLMs across eight families on a curated dataset of 205 TLA+ specifications, validated by both the SANY parser and TLC model checker. LLMs achieve up to 26.6% syntactic correctness but only 8.6% semantic correctness.
TLA-Prover: Verifiable TLA+ Specification Synthesis
Preference-Optimized Low-Rank Adaptation - Accepted at ICSOFT 2026
A 20-billion-parameter model trained with supervised fine-tuning and repair-based group-relative policy optimization (GRPO) for TLA+ specification synthesis. TLA-Prover achieves 30% semantic correctness — roughly 3.5× the 8.6% untuned baseline.
Research Areas#
Formal Specification and Verification
Building datasets, tooling, and infrastructure around TLA+ and other formal specification languages. Making model checking accessible through open pipelines and notebook-based workflows.
LLMs for Formal Methods
Evaluating whether large language models can generate semantically correct formal specifications. Identifying where LLMs fail on rigorous specification tasks and why.
Empirical Software Engineering
Studying software artifacts at scale: pre-trained model naming conventions, supply chain security, and development practices in real-world open-source systems.
Security and Systems
IoT security research including signal injection attacks on pairing protocols, plus HPC education tools and agentic tutoring systems for parallel computing.
Meet the Team#
Research Papers
Research Updates#
Friday, June 05, 2026: 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.
Saturday, May 16, 2026: 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.
Monday, 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).
Thursday, 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.
Friday, 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.
Saturday, 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.
Sunday, 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.
Friday, 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.
Thursday, 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.
Wednesday, 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.