News
← back to indexjust started caddying at Oak Park Country Club
I started selling clothes on Grailed. sourcing things, putting up listings, shipping orders
just started at Loyola. studying computer science with an information systems minor
I’m doing research at Loyola on how ChatGPT handles advanced Java concepts
working with Unchained AI this month, testing GPT-4 and figuring out why it gives the wrong answers
I’m taking care of the Alpha Kappa Psi website now. working on the homepage and member pages
just started at Loyola’s IT help desk. lots of support tickets and account access problems
I’m helping run the technical projects and workshops for Loyola’s AI Club this year
just started interning at EpiFinder. automating some of the internal workflows with Google Apps Script
I’m working on a marketing CX study for Microsoft this year
just wrote up my Hall of Fame predictor from the Google Cloud × MLB hackathon. it’s a decision tree trained on baseball stats
https://ericspencer.us/projects/mlb-hackathon/
https://ericspencer.us/projects/mlb-hackathon/
I made a VS Code extension to turn a whole repo into a text file for an LLM. got tired of pasting files one at a time
https://ericspencer.us/projects/flatten-repo/
https://ericspencer.us/projects/flatten-repo/
we’ve been working on sign language recognition in AI Club with Python and OpenCV. downloading all the videos taught me that you can run out of wifi
https://ericspencer.us/projects/sign-language/
https://ericspencer.us/projects/sign-language/
I got a Mulcahy Scholar stipend to work on LLMs and TLA+ at Loyola
https://ai4fm.cs.luc.edu/posts/eric-spencer-mulcahy-scholar-2025/
https://ai4fm.cs.luc.edu/posts/eric-spencer-mulcahy-scholar-2025/
just built a microwave demo to help teach TLA+ at Loyola. took two weeks. Spring Boot (Java) and Vaadin (also Java)
https://ericspencer.us/projects/interactive-microwave-tla/
https://ericspencer.us/projects/interactive-microwave-tla/
just started my summer internship at CCC. working with Vue and Spring Boot on their portal and an insurance claims dashboard
I’m joining AI4FM at Loyola to work on TLA+ and fine-tuning language models
I’m putting my apps under FROM AMERICA LLC now
https://fromamerica-llc.com
https://fromamerica-llc.com
just built Stock Genie, an iOS app for looking into stocks with AI
https://stockgenie.app
https://stockgenie.app
I’m building instxnt.xyz so you can make a storefront without paying a monthly subscription
https://instxnt.xyz
https://instxnt.xyz
I made Picaius because none of the photo editing apps on the App Store were doing what I wanted
https://picai.us
https://picai.us
just uploaded chattla-20b to Hugging Face. I’ve been fine-tuning it to write TLA+ specs
https://huggingface.co/EricSpencer00/chattla-20b
https://huggingface.co/EricSpencer00/chattla-20b
llm-tla.pdfour paper on whether LLMs can write correct TLA+ was accepted to and presented at ICSOFT 2026 in Porto
https://ai4fm.cs.luc.edu/papers/llm-tla-evaluation/
https://ai4fm.cs.luc.edu/papers/llm-tla-evaluation/
gsirs-poster.pdfBrian just presented the poster we worked on at GSIRS. it’s about how well LLMs actually do at writing TLA+
https://ai4fm.cs.luc.edu/posts/gsirs-llm-tla-poster-2026/
https://ai4fm.cs.luc.edu/posts/gsirs-llm-tla-poster-2026/
chattla-talk.pdfjust presented our ChatTLA+ work at Loyola’s undergraduate research symposium. these are my slides
https://ai4fm.cs.luc.edu/posts/chattla-presentation-2026/
https://ai4fm.cs.luc.edu/posts/chattla-presentation-2026/
just graduated from Loyola. BS in computer science, minor in information systems
I’ve been writing Coq and TLA+ specs for Rubik’s Snake. there’s a Python enumerator too
https://ericspencer.us/projects/rubix-snake-puzzle/
https://ericspencer.us/projects/rubix-snake-puzzle/
just put out the ChatTLA+ dataset. it has the verified training examples and the benchmark we used for the paper
https://ericspencer.us/projects/chattla-dataset/
https://ericspencer.us/projects/chattla-dataset/
I made a little macOS app for putting cover art on MP3s. drop in the audio and an image and it does the rest locally
https://ericspencer.us/projects/tunes2tube-mac/
https://ericspencer.us/projects/tunes2tube-mac/
I started making a programming language called Resilient. trying to put checked contracts and runtime recovery into the language itself. very much a research project
https://ericspencer.us/projects/resilient/
https://ericspencer.us/projects/resilient/
just joined HorneSci
https://hornesci.github.io
https://hornesci.github.io
tla-prover.pdfTLA-Prover just got accepted to ICSOFT 2026. this is the model I’ve been working on for generating TLA+ specs
https://arxiv.org/html/2606.06133v1
https://arxiv.org/html/2606.06133v1
tla-bench.pdfour TLA+-Bench preprint is out. we check the generated specs by actually running them. the dataset has 403 model-checked gold specs
https://arxiv.org/abs/2607.23425
https://arxiv.org/abs/2607.23425