Eric Spencer
News
2026-06-05tla-prover accepted at ICSOFT 2026. [link]
2026-04-17Presented ChatTLA+ at Loyola's Undergraduate Research & Engagement Symposium. [link]
2026-04Co-author on the GSIRS 2026 poster — first systematic eval of LLM→TLA+ synthesis. Paper Can LLMs Write Correct TLA+ Specifications? accepted to ICSOFT 2026 (Porto). Released chattla-20b on Hugging Face — 4,000+ downloads.
2025-05Awarded 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.
stem-playerBrowser-based DONDA stem player.
stemacle.comStemacle releases: web app, macOS downloads, iOS status, and source.
Blog
No posts yet.
Loading repos…
Experience
