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
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. Results show model size does not predict quality and code-specialized models consistently underperform on formal languages.
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#
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.