Work
Deep dives on the builds I'm proudest of. Each one foregrounds why the design is trustworthy as well as what it does, and they all ladder 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