Eric Spencer

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

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 (21)

GluCoPilotOpenAI Hackathon '25 — LLM copilot over Dexcom glucose data.Swift

reelforgemacOS app: Claude writes the script, ffmpeg burns the captions.TypeScript

als-signature-reversalReverse-signature drug repurposing for ALS on iPSC RNA-seq data.Jupyter Notebook

ascii-llm-trainingTraining a small LM purely on ASCII text.Python

comp388-llmCoursework: LLM systems (COMP 388).Python

llmjammerPython source obfuscator built to confuse code-scraping LLMs.Python

TerminalGPTTerminal-native LLM chat through OpenRouter.Python

ai-conversationTwo LLMs debate philosophy with each other.Python

ITS-RAG-botRetrieval-augmented assistant for an IT-service knowledge base.Python

Claude-architect-quizFree flashcards + practice quiz for the Anthropic architect exam.CSS

yeat-llmLyric-style language model experiment.Python

ollama-vibecodeLocal Ollama-driven code generation experiments.Python

ai-osExperimental LLM-driven operating-shell concept.Python

connect-4Chess-engine-style analyzer for Connect-4.Python

rl-agent-c4Reinforcement-learning agent for Connect-4.Python

rvc-artistRetrieval-based voice-conversion pipeline.Python

Intro-to-ttsMinimal text-to-speech in Python.Python

HandwritingHandwriting-recognition experiment.Python

fortnite-oneshotOne-shot scripting experiment.JavaScript

oneshot-hm2016One-shot generation experiment.JavaScript

audio-tabula-rasaAudio processing experiment.Python

macOS, iOS & Desktop (11)

tunes2tube-macmacOS app: cover art + audio in, MP4 music videos out.Swift

DexcomNavBarIcon-macosmacOS menu-bar widget surfacing live Dexcom readings.Python

GestureProof-of-concept Jarvis-style gesture control for macOS.Python

ChessStatsPulls and displays Chess.com statistics.Python

youtubeDLPersonal CLI / localhost YouTube audio+video downloader.Python

iOS-soundboardiOS soundboard app.Swift

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

DexValDexcom data validation / analysis utility.Python

T-squareSwift utility app.Swift

Systems, Languages & Tools (19)

git-key-guardianPre-commit guard that blocks secret keys from being committed.Shell

flatten-repoVS Code extension: flattens a repository into a single LLM-ready file.JavaScript

notify-agent-doneDesktop notification when a long-running agent finishes.TypeScript

UDP-server-binaryBinary-protocol UDP server in C++.C++

itch-parserC parser for ITCH-format market data.C

itch-parser-ericHand-rolled C variant of the ITCH market-data parser.C

reverse-xoroshiro128plusplusRecovering xoroshiro128++ PRNG state from output.Python

mc-carspotRust online-parking-spot simulator with switching costs.Rust

cubed-pack-solveSolver for a 3-D cube-packing puzzle.Python

auto-decodeHeuristic auto-detection and decoding of encoded text.JavaScript

palindrome-sentence-generatorGenerates whole paragraphs that read as palindromes.Python

grade-public-commitsAuto-grades student work from public commit history.Python

roman-numeral-converterRoman-numeral <-> integer converter.Java

etl-demoSmall ETL pipeline demonstration.Python

fg-scrapeTargeted web-scraping utility.Python

EmailExtractionBulk email-address extraction utility.Python

scala-workshopScala workshop materials and exercises.Scala

scala-hello-worldScala starter project.Scala

copilot-cli-testCopilot CLI evaluation sandbox.Shell

Web & Front-End (18)

EricSpencer00.github.ioSource of this site.HTML

pitchPitch-deck site.HTML

fb-cloneSystems-analysis Facebook clone (GraceNook).TypeScript

design-skillSingle-page editorial rendition of the personal site.HTML

ai4fmSource for the Loyola FMitF / AI4FM research-group website.Python

dev.EricSpencer00.github.ioPublic dev/staging of the personal site.HTML

archaic-radio-frontendFront-end for a retro internet-radio player.HTML

caterpillarStatic / interactive web piece.HTML

gcf-deSvelte data-engineering front end.Svelte

margaux-websitePersonal client website.

DailyTask-webDaily-task tracker web app.HTML

bio-ops-webBioinformatics ops web dashboard.JavaScript

sneaker-runBrowser endless-runner game.JavaScript

slot-machineBrowser slot-machine game.JavaScript

spa-webSingle-page web app scaffold.HTML

cone-siteStatic site project.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)

instxnt.xyzVisual AI-powered storefront builder.TypeScript

instxnt-mcpMCP server for instxnt.xyz — create storefronts through Claude, ChatGPT, Gemini.TypeScript

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 (12)

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.

My ~/.zshrcAnnotated walkthrough of my 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.