AI for Formal Methods

Loyola University Chicago’s research lab exploring the intersection of artificial intelligence and formal methods in software engineering. Established 2025.

• 
• 
• 

Publications

TLA+-Bench: An Execution-Grounded Benchmark and Dataset for Natural-Language to TLA+ Specification Generation

Arslan Bisharat, Eric Spencer, Brian Ortiz, Khushboo Bhadauria, Mujtaba Nazari, Beatriz Santos, Anisa Ramos, TaiNing Wang, George K. Thiruvathukal, Konstantin Läufer, Mohammed Abuhamad

TLA-Prover: Verifiable TLA+ Specification Synthesis via Preference-Optimized Low-Rank Adaptation

Eric Spencer, Arslan Bisharat, Brian Ortiz, Mujtaba Nazari, Khushboo Bhadauria, TaiNing Wang, George K. Thiruvathukal, Konstantin Läufer, Mohammed Abuhamad

Can LLMs Write Correct TLA+ Specifications? Evaluating Natural-Language-to-TLA+ Generation

Arslan Bisharat, Brian Ortiz, Eric Spencer, Khushboo Bhadauria, TaiNing Wang, George K. Thiruvathukal, Konstantin Läufer, Mohammed Abuhamad

Read more ›

Updates

June 05, 2026

TLA-Prover Paper Accepted to ICSOFT 2026

May 16, 2026

New Paper: TLA-Prover — Fine-Tuning LLMs for Verifiable TLA+ Specification Synthesis

May 11, 2026

Presented Two Posters at GCASR 2026

Read more ›

About

Meet the lab, our research focus, and the Loyola community behind AI4FM.

Get Involved

Find ways to contribute, collaborate, or join us as a student researcher.