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 — 13,500+ 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. Member of Technical Staff at HorneSci.

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.

▸ github · huggingface · linkedin · ai4fm.cs.luc.edu · résumé · email

Selected Work

TLA+ GeneratorPlain English in, model-checked TLA+ out — a self-correcting loop that runs until SANY and TLC pass and the invariant holds.

tla-w4-diamond-goldVerifier-gated TLA+ SFT corpus — 5,010 examples that survived the W4 diamond-gold filter.

ResilientStatically-typed compiled language for safety-critical embedded systems.

TLA-ProverVerifiable TLA+ specification synthesis via preference-optimized low-rank adaptation.

AuraOSExperimental LLM-driven operating-shell concept.

FormaLLMToolkit for evaluating LLMs on formal-specification synthesis.

stemacle.comStemacle releases: web app, macOS downloads, iOS status, and source.

paper-digestCloudflare Worker that ranks each day's new arXiv papers against plain-English interests, with a keyword fallback so the API never breaks.