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. Same discipline, new substrate. 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
- 7 open-source tools live on PyPI
- A transparency log standing watch on federal data
- 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
- pip install congruent-eq
- 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
- pip install toroid
- 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
- pip install kinescope
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
- Research
Stemma — a laboratory for evolving invented languages
Treat a constructed language as a living system: define a proto-language's phonology, run ordered sound-changes across simulated centuries, fork daughter tongues, and trace any descendant word rule-by-rule back to its ancestor — deterministic, seeded, and fully tested.
- Rust
- Deterministic simulation
- 8-crate workspace