Work
Deep dives on the builds I'm proudest of. Each one foregrounds why the design is trustworthy — not just what it does — and ladders to the same claim: correctness under complexity, and the discipline to prove it.
- 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
- Solo design & build
Crucible — turning test-time compute into measured accuracy (or an honest negative)
On real MATH-500 (3 seeds), search lifts a frozen 1.5B model from 38% pass@1 to 70% with an oracle verifier at N=8 — and every headline number, positive or negative, regenerates offline from committed cassettes.
- best-of-N → beam → MCTS, one interface
- MATH-500: pass@1 38% → oracle 70% @ N=8
- Headline numbers replay offline in CI
- Solo design & build
Verderer — a provable record of how public data changes
Turns "did this dataset quietly change?" into something you can prove: every observation is attested in an append-only log, and a downloadable bundle verifies offline against independent anchors.
- Rust Merkle log + WASM verifier
- Verify offline — trust nobody
- Fuzzed differ · 100k-leaf proofs
- Solo design & build
Gatecheck — a testing layer for LLM systems
Turns "does the new prompt/model feel better?" into a number you can diff, gate a pull request on, and watch over time — wired into CI, priced per run.
- Deterministic graders gate CI
- Ollama / OpenAI / Anthropic / Bedrock
- 3 runtime deps, no SaaS, no Node