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-04Released chattla-20b on Hugging Face. 13,500+ downloads. [model]
2026-04Paper Can LLMs Write Correct TLA+ Specifications? accepted to ICSOFT 2026 (Porto). [paper]
2026-04Co-author on the GSIRS 2026 poster: first systematic evaluation of LLM to TLA+ synthesis. [poster]
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. Erdős number: 5.
Selected Work
Not HotdogHot dog or not hot dog: a 136,417-parameter int8 CNN with hand-written JavaScript kernels, zero dependencies, and bit-exact parity against a NumPy reference.
ResilientStatically-typed compiled language for safety-critical embedded systems. Z3-verified contracts, no_std runtime, ships to Cortex-M and RISC-V.
HST-StudioA delta-aware sparse linear algebra runtime, and the tooling around it.
tlakitPython and notebook client for the TLA+ toolchain. Drives SANY, TLC, and TLAPS from a cell without reimplementing TLA+ semantics.
paper-digestCloudflare Worker that ranks each day's new arXiv papers against plain-English interests, with a keyword fallback so the API never breaks.
Blog
No posts yet.
Loading repos…
Loading Hugging Face models…
Experience
