Eric Spencer

Every public repository from github.com/EricSpencer00 plus org work at LUC-AI4FM and FROM AMERICA.

Recent Work (13)

Shipped in the last month, ordered by how hard it was to pull off.

TLA+ GeneratorPlain English in, model-checked TLA+ out — a self-correcting loop that runs until SANY and TLC pass and the invariant holds.Python
colibriRuns GLM-5.2 (744B MoE) on a 25GB-RAM consumer machine — pure C, zero deps, experts streamed from disk.C
Not HotdogA 136K-parameter int8 CNN running on hand-written JavaScript kernels — no TensorFlow, no WASM, no dependencies. Hot dog or not hot dog.JavaScript
Claude-of-DutyA Call-of-Duty-quality FPS in Three.js, built from a single prompt. forkJavaScript
tof-auditPhysics-based location audit: times light in fiber to eight cities and triangulates the browser on a 3D globe.HTML
tla-microwaveInteractive TLA+ microwave — the entire state space in your browser, learned by clicking buttons.TypeScript
polymarket-whale-trackerFinds the algorithmic whales on Polymarket and emits copy-trade signals. Read-only — it watches, it does not place bets.Python
paper-digestInterest-matched research papers on Cloudflare Workers — semantic ranking, honest thresholds, keyword fallback.TypeScript
usage-badgeLive README badge for AI coding usage — subscription limits plus token/cost across agents, in one Worker.Python
chess-coachPersonal chess coach: Chess.com history + Stockfish analysis + play-vs-engine debrief.HTML
openclaw-skill-paper-digestOpenClaw/picoclaw skill: semantically-ranked recent papers by interest, with TL;DRs.
openclaw-skill-stockgenieOpenClaw/picoclaw skill: StockGenie daily AI stock pick.
hardtekk-generatorGenerative hardtekk in the browser.Python
cad-bench-submissionSubmission portal for the Parametric CAD Bench leaderboard.

Formal Methods & Verification (15)

ResilientStatically-typed compiled language for safety-critical embedded systems with Z3-verified contracts.Rust
rubix-snake-puzzleFormal verification (Coq + TLA+) of Rubik's-Snake state reachability.Rocq Prover
interactive-microwave-tlaBrowser-based TLA+ microwave — a gentle first model-checking demo.Java
FormaLLMToolkit for evaluating LLMs on formal-specification synthesis. forkTLA
chattla-dataset-anonAnonymized dataset release for the ChatTLA+ paper.
Resilient-examplesMission-critical example programs for Resilient.Shell
tla-formal-generationPipeline for generating TLA+ specs from natural language.Python
tla-walk-in-ovenTLA+ specification of a walk-in-oven control system.TLA
tla-dexcom-g7TLA+ specification of Dexcom G7 CGM session lifecycle.TLA
c4-fmitfTLA+ formal model of Connect-4 game mechanics.TLA
tla-laptopTLA+ model of laptop power/state transitions.TLA
fm-cb-gameFormally-modeled combinatorial board game in TLA+.TLA
TLAJVMExperiments running TLA+ / TLC tooling on the JVM.Java
rocqPlayground for the Rocq (Coq) proof assistant.Coq
goldbach-conjBrute-force verification of the strong Goldbach conjecture to 1e9.Python

AI, LLMs & Machine Learning (22)

AEO QueriesChrome extension that records the exact search queries ChatGPT, Claude and Perplexity issue for a prompt.JavaScript
GluCoPilotOpenAI Hackathon '25 — LLM copilot over Dexcom glucose data.Swift
als-signature-reversalReverse-signature drug repurposing for ALS on iPSC RNA-seq data.Jupyter Notebook
ITS-RAG-botRetrieval-augmented assistant for an IT-service knowledge base.Python
reelforgemacOS app: Claude writes the script, ffmpeg burns the captions.TypeScript
llmjammerPython source obfuscator built to confuse code-scraping LLMs.Python
ascii-llm-trainingTraining a small LM purely on ASCII text.Python
yeat-llmLyric-style language model experiment.Python
rvc-artistRetrieval-based voice-conversion pipeline.Python
ai-osExperimental LLM-driven operating-shell concept.Python
rl-agent-c4Reinforcement-learning agent for Connect-4.Python
connect-4Chess-engine-style analyzer for Connect-4.Python
TerminalGPTTerminal-native LLM chat through OpenRouter.Python
Claude-architect-quizFree flashcards + practice quiz for the Anthropic architect exam.CSS
ai-conversationTwo LLMs debate philosophy with each other.Python
ollama-vibecodeLocal Ollama-driven code generation experiments.Python
comp388-llmCoursework: LLM systems (COMP 388).Python
HandwritingHandwriting-recognition experiment.Python
Intro-to-ttsMinimal text-to-speech in Python.Python
audio-tabula-rasaAudio processing experiment.Python
fortnite-oneshotOne-shot scripting experiment.JavaScript
oneshot-hm2016One-shot generation experiment.JavaScript

macOS, iOS & Desktop (11)

tunes2tube-macmacOS app: cover art + audio in, MP4 music videos out.Swift
GestureProof-of-concept Jarvis-style gesture control for macOS.Python
DexcomNavBarIcon-macosmacOS menu-bar widget surfacing live Dexcom readings.Python
DexValDexcom data validation / analysis utility.Python
iOS-soundboardiOS soundboard app.Swift
T-squareSwift utility app.Swift
ChessStatsPulls and displays Chess.com statistics.Python
youtubeDLPersonal CLI / localhost YouTube audio+video downloader.Python
apple-music-widgetNow-playing Apple Music web widget.JavaScript
ReserveLibraryRoomAutomates Loyola library-room reservations.Python
WindowBlockerForTDX-MacOSSafari script blocking the TDX ticketing pop-out on macOS.JavaScript

Systems, Languages & Tools (21)

reverse-xoroshiro128plusplusRecovering xoroshiro128++ PRNG state from output.Python
itch-parser-ericHand-rolled C variant of the ITCH market-data parser.C
itch-parserC parser for ITCH-format market data.C
mc-carspotRust online-parking-spot simulator with switching costs.Rust
UDP-server-binaryBinary-protocol UDP server in C++.C++
cubed-pack-solveSolver for a 3-D cube-packing puzzle.Python
flatten-repoVS Code extension: flattens a repository into a single LLM-ready file.JavaScript
git-key-guardianPre-commit guard that blocks secret keys from being committed.Shell
notify-agent-doneDesktop notification when a long-running agent finishes.TypeScript
palindrome-sentence-generatorGenerates whole paragraphs that read as palindromes.Python
auto-decodeHeuristic auto-detection and decoding of encoded text.JavaScript
grade-public-commitsAuto-grades student work from public commit history.Python
1RMOne-rep-max calculator: median of seven estimators, installs to a phone home screen and runs offline.HTML
DDIA Learning LabDesigning Data-Intensive Applications study notes and quiz drill.HTML
etl-demoSmall ETL pipeline demonstration.Python
fg-scrapeTargeted web-scraping utility.Python
EmailExtractionBulk email-address extraction utility.Python
roman-numeral-converterRoman-numeral <-> integer converter.Java
scala-workshopScala workshop materials and exercises.Scala
scala-hello-worldScala starter project.Scala
copilot-cli-testCopilot CLI evaluation sandbox.Shell

Web & Front-End (19)

stemacleBrowser-based stem player — splits a track into its parts in the tab, no upload.JavaScript
fb-cloneSystems-analysis Facebook clone (GraceNook).TypeScript
gcf-deSvelte data-engineering front end.Svelte
ai4fmSource for the Loyola FMitF / AI4FM research-group website.Python
archaic-radio-frontendFront-end for a retro internet-radio player.HTML
bio-ops-webBioinformatics ops web dashboard.JavaScript
design-skillSingle-page editorial rendition of the personal site.HTML
EricSpencer00.github.ioSource of this site.HTML
pitchPitch-deck site.HTML
caterpillarStatic / interactive web piece.HTML
sneaker-runBrowser endless-runner game.JavaScript
slot-machineBrowser slot-machine game.JavaScript
DailyTask-webDaily-task tracker web app.HTML
margaux-websitePersonal client website.
spa-webSingle-page web app scaffold.HTML
cone-siteStatic site project.HTML
dev.EricSpencer00.github.ioPublic dev/staging of the personal site.HTML
uzzGeneratorProcedurally generates 'uzz'.Python
EricSpencer00GitHub profile README.HTML

Coursework, Hackathons & Misc (12)

HackIllinois26HackIllinois 2026 hackathon project.TypeScript
MLB-HackathonGoogle Cloud x MLB hackathon — Hall of Fame predictor.Python
LoyolaHACKCTA Transit Tracker — Loyola hackathon.HTML
SerenityWildHacks 2024 project.JavaScript
HealthUp-COMP 322 semester-long mobile health app.JavaScript
AoC2025Advent of Code 2025 solutions.Python
comp371-team8-activityProgramming languages (COMP 371).Scala
Comp272ProjectsData structures (COMP 272).Java
COMP330Group5Coursework group project (COMP 330).Java
BlackJackGameBlackjack game.Python
AnagramSolverV1Anagram solver.Java
ChatJava chat application.Java

LUC-AI4FM (12)

ChatTLAFine-tuning open-source LLMs to generate verifiable TLA+ formal specs.Python
FormaLLMToolkit for evaluating LLMs on formal-specification synthesis.TLA
eric-paperICSOFT paper: ChatTLA+ fine-tuning for verifiable TLA+ specifications.TeX
chattla-spec-gen-paperChatTLA+ NeurIPS 2026 paper.TeX
chattla-gpt-oss-paperFine-tuning gpt-oss-20b for verifiable TLA+ specs.TeX
TLA-ExtractionExtracting TLA+ specifications from research papers.Python
tla-dataset-pipelineDataset pipeline for TLA+ specification data.Python
tla_benchmarkBenchmark suite for TLA+ spec generation.
tla_descriptionTLA+ description corpus for LLM training.
ralph-tlaRalph TLA+ experiments.
paper-parseResearch paper parsing utilities.Python
webpageAI4FM research group website source.HTML

FROM AMERICA (28)

picaiAI photo platform.TypeScript
StockGenieStock analysis iOS app.JavaScript
stockgenie-webStockGenie static site: Privacy & Terms.HTML
fair-shareReceipt scanner and bill splitter iOS app.Jupyter Notebook
FreeLockiOS app.Swift
ealing-capitalEaling Capital site redesign (Astro + Tailwind).Astro
wildhacks-26WildHacks 2026 entry.Swift
glucopilot-v2GluCoPilot v2 iOS app.Swift
cs-glucopilotGluCoPilot case study.Python
DailyTaskiOS daily task tracker.Swift
ai-headshotsAI headshot generator.TypeScript
arb-bot-liveLive arbitrage bot.C++
autotradeAutomated trading system.Python
b-slangLanguage experiment.TypeScript
suno-ipadSuno iPad interface.Swift
chambr-webChambr website: privacy, terms, landing page.HTML
splithound-webSplitHound web presence.HTML
FreeLock-webFreeLock web presence.HTML
Panda-RolliOS game app.Swift
HideAndSeekiOS game.Swift
RogueiOS game.Swift
Private-WhisperPrivate speech-to-text iOS app.Swift
idle-fishiOS idle game.Swift
IdleHeroesiOS idle game.Swift
famous.mojiEmoji app.CSS
from-america.github.ioFROM AMERICA LLC corporate site.HTML

Misc & Demos (13)

GTA V Gold Medal ChecklistEvery mission's gold-medal requirements in one checklist that remembers what you've cleared.TypeScript
Game of LifeConway's Game of Life — canvas demo.JavaScript
BlackJackBrowser blackjack with fake money.JavaScript
Chess.com StatsPulls and visualizes Chess.com stats.Python
Pixel ProfileGitHub profile-picture generator.JavaScript
Wiki RaceWikipedia speed-run game.JavaScript
Chess GameBrowser chess game.JavaScript
Skeuomorphic DeskAn editorial / skeuomorphic project desk.HTML
Song RecommenderPython recommender that beats Spotify's mid suggestions.Python
How to tell if it's AIHeuristic essay on spotting AI-generated text.
~/.zshrcAnnotated walkthrough of a shell config.Shell
AoC 2025Advent of Code 2025 notes.Python
ChatTLA+ DatasetNotes on the ChatTLA+ dataset release.

Contributions & Forks (20)

WhiskyA modern Wine wrapper for macOS built with SwiftUI.Swift
BrowserOSBrowserOS — an open-source agentic web browser.Python
vscodeVisual Studio Code.TypeScript
tlaplusTLC model checker for TLA+.Java
typescript-goNative port of TypeScript.Go
cli-githubGitHub's official command line tool.Go
linguistLanguage Savant.Ruby
ExamplesA collection of TLA+ specifications.TLA
CSAPP-LabSolutions to CSAPP & CMU 15-213 labs.C
harvard-cs50w-2020CS50's Web Programming.HTML
trash-alloyFilesystem trash example from Alloy 6 book.Alloy
Sign-Language-RecognitionSpring 2025 Sign Language Recognition Model.Python
MovieRec-F24Fall 2024 movie rec project.Python
March-Madness-MLMachine-learned bracketology.Python
simpleconcurrency-tlaTLA+ concurrency example.TLA
echotest-scalaScala echo test.Scala
shapes-oo-scalaScala OO shapes example.Scala
argon-design-system-angularArgon design system port.SCSS
claude-architect-exam-prepArchitect exam prep materials.
Hello-WorldFirst repo on GitHub.

Writeups & Archive (25)

Older projects and coursework that have a writeup here but no active repo listing above.

AI HeadshotsReplicate Wrapper
Anagram SolverScrabble Inspired Anagram Solver
Anagram Solver V2Scrabble Inspired Anagram Solver
Ancestry Tree Java ExampleAncestry Tree Java Example — project by Eric Spencer.
BrightBet.techAn AI-powered trade and prediction analysis platform built for HackIllinois 2026.
ChatGPT ResearchResearch with v3.0 and how it could possibly teach those new to Java Data Structures
Cubed Pack SolverA solver for packing 54 T-tetracubes into a 6x6x6 cube using Knuth's Dancing Links algorithm.
Daily Task - Wellness TrackerA habit manager for daily consistency.
DexValA project analyzing Dexcom CGM data beyond the standard Clarity app.
Machine Learning Fraud IdentifierAnalyze different Machine Learning algorithms to identify fraud within a classified dataset
Machine Learning Fraud IdentifierAnalyze different Machine Learning algorithms to identify fraud within a classified dataset
Free Time Calculator in JavaA Java program to find overlapping free time for up to four people.
Goldbach ConjectureVerifying the Goldbach Conjecture by brute force for every even number up to 1 billion.
COMP322 Final Project ReflectionCOMP322 Final Project Reflection — project by Eric Spencer.
Iterative Maze Solver ExampleIterative Maze Solver Example — project by Eric Spencer.
Loyola ITS RAG BotA voice-first RAG chatbot trained on Loyola's ITS knowledge base, built after two years of answering the same tickets.
Researching ChatGPT with ChatGPTResearching ChatGPT with ChatGPT — project by Eric Spencer.
Movie Recommendation WebsiteA movie recommendation website developed as part of the Loyola AI Club's Fall 2024 project.
One Rep Max CalculatorCalculate your One Rep Max
Recursive Maze Solver ExampleRecursive Maze Solver Example — project by Eric Spencer.
SerenityA mental wellness application developed at Northwestern's Wildhacks Hackathon.
AI Sign Language InterpreterA Simple Sign Language Recognition App using OpenCV
TLA+ Model of Dexcom G7A formal TLA+ specification of the Dexcom G7 continuous glucose monitor's behavior and safety properties.
TLA+ Model of a LaptopA formal TLA+ specification modeling a laptop's power states, battery, lid, thermals, and auto-suspend.
TLA+ Model of a Walk-In OvenA formal TLA+ specification of a walk-in industrial oven with a focus on safety interlocks.