I build automated systems that stay correct under complexity — and I can prove it.
I bring formal-methods rigor from silicon design flows to AI systems — equivalence proofs, deterministic replay, coverage, eval gates. Correctness under complexity is the through-line. On the side: real-time graphics, simulation, and games.
Independent — building open verification tooling for AI systems. Open to senior roles in verification, dev-tooling, and AI reliability.
- Ex-Synopsys — EDA automation at production scale
- 6 public verification tools on GitHub
- B.S. CS — WSU Vancouver
Selected work
All case studies →- Solo design & build
Congruent — proving AI-rewritten code equivalent (or finding the input that breaks it)
Given an original function and an AI-rewritten one, Congruent returns a real answer — proven equivalent within bounds, or the concrete input where they disagree — never "passed the tests, probably fine."
- difftest → symbolic exec → Z3 SMT
- 10/10 fixtures decided, 0 unsound
- Every verdict carries its bound
- Solo design & build
Toroid — an agent that writes and proves correctness properties for chips
Point Toroid at a Verilog module and its spec: every property comes back PROVEN, BOUNDED-PASS to a stated depth, or FALSIFIED with a concrete counterexample trace — and it catches an injected FIFO bug end-to-end.
- LLM proposes → Yosys/SymbiYosys disposes
- 9 props synthesized live, 5/5 asserts proven
- PROVEN only from an unbounded engine
- Solo design & build
Kinescope — a flight recorder for AI agents (deterministic replay, counterfactual forks)
An agent failure that was unreproducible replays bit-for-bit from a local trace — scrub to the step that went wrong, override that one decision, and watch the branched run complete live.
- 62 offline tests, zero network
- Anthropic / OpenAI / Gemini
- Real run replays bit-for-bit in CI
Featured projects
All projects →- Graphics
Cambrian — a 3D artificial-evolution toy
Grow a random alien from a generative genome, then mutate and select it across generations — steer a blob toward a rodent toward a shark. Purely for the fun of it.
- TypeScript
- React Three Fiber
- Vite
- Games
Omnia — a deterministic "everything simulator"
A living town of hundreds of agents who work, marry, and die across generations — an ECS simulation with deterministic replay, invariant checking, and local-LLM agent minds kept off the hot path.
- TypeScript
- ECS
- Ollama
- Games
Tavern — AI companions for Warcraft 3
Free, offline local-LLM teammates and opponents for Warcraft 3: they chat, take voice commands, strategize over AMAI, and trash-talk — all on a LAN, no cloud.
- Python
- TypeScript → Lua
- Ollama
- whisper.cpp / Piper