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. [model]

2026-04Paper Can LLMs Write Correct TLA+ Specifications? accepted to and presented at ICSOFT 2026 (Porto). [paper]

2026-04Co-author on the GSIRS 2026 poster about systematic evaluation of LLM to TLA+ synthesis. [poster]

2025-05Awarded the Mulcahy Scholar stipend for LLM-based TLA+ research. [link]

see all news

About

Graduate researcher at Loyola University Chicago, working on formal methods and large language models. Member of Technical Staff at HorneSci.

At the AI4FM / FMitF group under Prof. Konstantin Läufer: 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.

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

Research

TLA+ specification generationLanguage models and formal verification

ChatTLA+ datasetTraining data for TLA+ generation

ResilientProgramming language with Z3-verified contracts

Papers, models, and datasets

Selected Work

PalindromePalindromic sentence generator

Not HotdogBrowser image classifier

I Paid For This ShirtShirt price printed on shirt

Loading repos…

Loading Hugging Face models…

Open Sourcechattla-20bgpt-oss-20b fine-tuned to write verifiable TLA+ specifications.huggingface.co/EricSpencer00The ChatTLA+ models and the datasets they were trained on.github.com/EricSpencer00Formal methods, LLM tooling, compilers, macOS and iOS apps.All projectsEvery public repository and writeup, by category.