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
- 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
- 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
- pip install crucible-ttc
- Solo design & build
Verderer — a provable record of how public data changes
It stands watch unattended, every six hours, against real federal data — and it has already attested its first change in the wild (a content edit to the FEMA National Risk Index) into an append-only log a stranger can verify offline, trusting neither the government nor me.
- Live & unattended — every 6 hours
- C2SP Merkle log · offline WASM verify
- Bitcoin + RFC 3161 time anchors
- First real change attested · FEMA NRI
- 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
- pip install gatecheck
- Solo design & build
Manifold — constrained-random coverage testing for AI agents
Point Manifold at an agent and it generates seeded, fault-injected scenarios, measures functional coverage of a behavior space you declare, and biases new runs toward the gaps — reaching full coverage in roughly 20× fewer scenarios than uniform random, every failure replayable from its exact seed.
- Coverage-directed: ~4× fewer runs to 90%
- pass^k flakiness · seeded repro · shrinker
- 7 invariants · live-verified on real agents
- pip install manifold-cov