I study how language models reason and respond to training, and put AI agents to work on hard, checkable problems: formal proofs, faster code, real bugs.
Write-ups, models and every repo: casella.dev
Each write-up lists its model, data, code and open issues.
- I used agents and Lean to cut a compiled PyTorch workload’s runtime by 26% · code · PR
Agents declared atorch.compilekernel’s size arguments 32-bit, proved in Lean when that is exact, and cut a changing-shape workload’s time by 26% on one L4. - I used agents to find 25 bugs in free-threaded CPython
Agents confirmed 25 bugs in the no-GIL build, with no earlier report found for 18. TLAPS and Lean proofs of the locking model held; replays of real runs showed five places CPython leaves it. - I used formal verification and agents to make an algorithm 105× faster and prove it behaves the same
Seven rewrites of deliberately slow Dafny routines verified against a frozen spec; one ran 105× faster on a workload it never saw. - A 50-step RL update reduces categorical sampling bias · code
Fifty RL steps on one random-integer task moved nine untrained pick-one tasks toward uniform on Qwen3-30B-A3B-Instruct. - Hidden-state probes outperform self-reported confidence · code
A linear probe on Llama 3.1 8B’s hidden states ranks claim correctness better than the model’s stated confidence. - Panel-style reasoning trades accuracy for shorter completions and one RL run on sometimes-solvable problems · code
All seven: casella.dev/research.html
- Dynamic Workflows on Codex — A Claude Code skill: describe a task, and Claude writes a multi-agent workflow script, runs it on Codex agents instead of Claude subagents, and shows the run as a live map.
- nanochat-mlx — Train a small chatbot from scratch on Apple Silicon, from tokenizer training to a chat interface.
- Qwen Scope Lab — A browser workbench for sparse-autoencoder interpretability on Qwen3.5-2B, running on the Mac through MLX.
ML on Apple Silicon: gemma4-m4-pro · train-gemma4-sudoku-on-your-macbook · ttt-discover-autoresearch-mlx
Research code: bsf-steering · society-of-thought-bench · hypothesis_forge · adaptive_rag_rlm · autoresearch-evo · Proofgrade
macOS menu bar apps (TabPilot, SunShift, SafariMarkdown, GhostLabel, PasteForge, TextDrop and ClipDrop install with brew install scasella/tap/<app>, via homebrew-tap):
TabPilot · SunShift · SafariMarkdown · GhostLabel · PasteForge · TextDrop · ClipDrop · DiskPulse · PortSentry · ProcessBeacon · BrewPilot
- Random-choice adapter — a Qwen3-30B-A3B LoRA for experiments with fixed-list sampling behavior.
- Panel-reasoning adapter — the Qwen3-30B-A3B LoRA from the accuracy and completion-length comparison.
Personal projects. Not affiliated with or endorsed by my employer. Contact: LinkedIn.