Eric Spencer

Papers, talks, and tools from my work at the AI4FM / FMitF group at Loyola University Chicago, under Prof. Konstantin Läufer.

Papers

2026Can LLMs Write Correct TLA+ Specifications? Accepted to ICSOFT 2026 (Porto). [link] [repo]
2026ChatTLA+ spec-gen paper (NeurIPS 2026 submission). [repo]
2026ChatTLA+ gpt-oss paper — fine-tuning gpt-oss-20b for verifiable TLA+ specs and TLAPS proofs. [repo]

Presentations & Posters

2026-04-17Presented ChatTLA+ at Loyola's Undergraduate Research & Engagement Symposium. [link]
2026-04-11Co-author on the GSIRS 2026 poster — first systematic eval of LLM→TLA+ synthesis. [link]

Models & Datasets

2026-03chattla-20b on Hugging Face — fine-tuned 20B model (SFT+GRPO on gpt-oss-20b) for TLA+. 4,000+ downloads. [model]
2026chattla-dataset-anon — anonymized dataset for the ChatTLA+ paper. [repo]

Tools

2026FormaLLM — toolkit for evaluating LLMs on formal-specification synthesis. [repo]
2025TLA-Extraction — extracting TLA+ specs from research papers. [repo]

Awards

2025Awarded the Mulcahy Scholar stipend for LLM-based TLA+ research. [link]
2022Awarded the Presidential Scholarship at Loyola University Chicago.