AI-Written

A statically-typed compiled language for safety-critical embedded systems, with Z3-verified contracts and self-healing runtime blocks

Coq (Rocq) and TLA+ specifications of the Rubik’s Snake state space — 4^23 configurations, formally

A local macOS app that drops a cover image and audio files in, and gives you back MP3s with the cover embedded as ID3v2 artwork — no account, no upload.

Free flashcards and practice quiz for the Anthropic Claude Certified Architect exam.

The dataset release for the ChatTLA+ paper — SFT corpus and benchmark for TLA+ spec generation, posted anonymized for blind review.

Two homeworks from Loyola’s special-topics LLMs class: prompting GPT-2 and comparing base vs instruction-tuned Qwen.

A voice-first RAG chatbot trained on Loyola’s ITS knowledge base, built after two years of answering the same tickets.

A solver for packing 54 T-tetracubes into a 6x6x6 cube using Knuth’s Dancing Links algorithm.

My Advent of Code 2025 attempt in Python. Got six days in before life took over.

A formal TLA+ specification of a walk-in industrial oven with a focus on safety interlocks.

Verifying the Goldbach Conjecture by brute force for every even number up to 1 billion.

A formal TLA+ specification modeling a laptop’s power states, battery, lid, thermals, and auto-suspend.

A formal TLA+ specification of the Dexcom G7 continuous glucose monitor’s behavior and safety properties.

Early exploratory repo for generating TLA+ specs from natural-language requirements with an LLM, with a TLC harness wired in. The scaffold that eventually grew into ChatTLA+.

A toy transformer that reads pyfiglet ASCII art and tries to spit the original word back out. Calling it an LLM is generous.

A tiny Rust simulator for the online parking-spot problem with switching costs.

A SwiftUI soundboard app I built in an afternoon to get more comfortable with iOS.

A small Flask app that pulls Chess.com’s public API and graphs your rating history.

A proof of concept Jarvis-style macOS controller that takes voice commands and hand gestures from the webcam.

A toy where two local Ollama models loop on consciousness until one of them gives up

A VS Code extension I made when I kept running out of Copilot credits — flattens a repo into one .txt file you can paste into a free LLM.

A real-time bus and train tracking system built during Loyola’s Hackathon.

A scikit-learn decision tree that guesses whether a current MLB player would get voted into Cooperstown, built for the Google Cloud x MLB hackathon.

A small Python CLI for chatting with OpenAI and running English-to-Bash commands from the terminal. The thing I actually open when I want to talk to a model.