Eric Spencer
News
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]
2026-04Paper Can LLMs Write Correct TLA+ Specifications? accepted to ICSOFT 2026 (Porto). [link]
2026-03Released chattla-20b on Hugging Face — 4,000+ downloads. [link]
2025Awarded the Mulcahy Scholar stipend for LLM-based TLA+ research. [link]
About
Graduate researcher at Loyola University Chicago, working at the intersection of formal methods and large language models.
At the AI4FM / FMitF group under Prof. Konstantin Läufer: first systematic evaluation of LLM-generated TLA+, the chattla-20b model, and a paper at ICSOFT 2026. Outside the lab: the Resilient compiler, macOS and iOS apps, and FROM AMERICA LLC.
Selected Work
chattla-20bFine-tuned 20B model (SFT+GRPO on gpt-oss-20b) for TLA+ generation.
ResilientStatically-typed compiled language for safety-critical embedded systems.
ChatTLA+ paperFirst systematic evaluation of LLM-generated TLA+ — accepted to ICSOFT 2026.
AuraOSExperimental LLM-driven operating-shell concept.
FormaLLMToolkit for evaluating LLMs on formal-specification synthesis.
Blog
No posts yet.
Loading repos…
Experience
