About AI4FM#
The AI for Formal Methods (AI4FM) research group is part of the Department of Computer Science at Loyola University Chicago. We are a community of researchers, students, and collaborators advancing AI-assisted formal methods, rigorous system design, and reproducible research tools.
Mission#
Our mission is to conduct formal methods research that bridges logic, mathematics, and real-world computing systems - with an emphasis on making these techniques practical, accessible, and reproducible.
We pursue this mission by:
Conducting formal methods research grounded in logic and mathematics, applied to real systems
Fostering collaborative projects across Computer Science and related fields
Building open tools, datasets, and workflows for formal methods, AI/ML, and LLM research
Supporting student research experiences through accessible open-source projects
Research Areas#
Formal Methods and Specification Languages#
We work with TLA+, a formal specification language designed to model and verify concurrent and distributed systems. Our research includes building datasets, tooling, and pipelines around TLA+ to support large-scale analysis and reproducible experimentation.
Large Language Models for Formal Methods#
A central focus of our group is applying large language models (LLMs) to formal methods tasks - from generating TLA+ specifications to reversing formal models back into natural language documentation. This line of work explores how modern AI can assist with rigorous system design while maintaining the correctness guarantees that formal methods provide.
Empirical Software Engineering#
We study software artifacts, naming conventions, and development practices through empirical methods. Our work on pre-trained model (PTM) naming and software supply chain security examines how engineering quality and reproducibility manifest in real-world open-source systems.
Security and Systems#
Members of our group work on IoT security (signal injection attacks, pairing protocols), high-performance computing, and distributed systems - contributing security-aware design principles to systems research.
Research Philosophy#
We believe research tools should be open, reproducible, and practically grounded. All of our work is published as open-source software or open datasets wherever possible. We value rigorous methodology, collaborative development, and student participation at every stage.