Selected work
A recurring pattern: systems you can verify.
Four domains, one through-line — deterministic, verifiable systems taken from applied research all the way to working, adversarially-tested implementations. Each comes with real evidence you can open and check.
Distributed Trust
FlagshipCairn
Serverless trust for disconnected systems — post-quantum end to end.
Every production trust system depends on a server that is always reachable. Cairn removes that assumption: devices and agents admit and revoke each other directly — offline, post-quantum, with a signed and replayable audit of every decision. The deployable application is identity continuity — keep authenticating and still revoke a compromised device while Okta, Entra or AD is down, with a signed record of who was admitted during the outage. The engine was hardened where conditions are worst: a live 4-node mesh across Toronto, New York and London, real NATO battalion-mobility data, and a drone fleet under emulated jamming.
Machine-Checked Code
Attestral — published research
Code that carries its own proof.
The verifier in the loop with the AI: the model proposes, a separate checker adjudicates through a ladder of 10 languages and 6 formal verifiers (Kani, CBMC, Lean 4, Dafny, F*, TLA+), and only a passing check mints an ed25519-signed certificate anyone can re-run offline. Flagship demonstration: when an AI helped disprove the 87-year-old Jacobian Conjecture in July 2026, Attestral certified the counterexample’s entire structural anatomy — 43 signed certificates, 20 of them Lean 4 kernel proofs, published with a DOI. It also caught three of our own errors before they shipped, which is the point.
Open Source
bitrep — Rust · JS · Python library
Any order. Any hardware. Same bits.
Order-invariant, bit-identical floating-point reductions: exact mergeable sums with a canonical 289-byte state. Proved in Lean, checked by Kani, fuzzed against an independent oracle, and pinned to one SHA-256 across x86-64, ARM64, Windows and WebAssembly in CI on every commit. The open work sample — the same verifiable-systems discipline as the closed projects, with every claim inspectable.
Deterministic Memory
Neruva — internal R&D
Memory you can replay.
The reproducible memory substrate I built and run across my own projects: deterministic recall (same query, same answer, every time), enforce-deny corrections, provenance and citations on every result, and snapshot/replay audit of memory state. Not a commercial product — internal tooling, shown here as evidence of the same verifiable-systems pattern applied to AI memory.
How it's proven
Every result is produced with sound, audited tools on real public data, with a documented test method — the evidence, not just claims. See the full stack, datasets, and red-team methodology on the Cairn Technical Validation page.
Results shown · mechanism protected
Cairn's design, source, and formal proofs are proprietary and available under NDA. Attestral and Neruva are internal tooling, shown here as evidence rather than as products for sale.
Want to go deeper?
Open to senior / principal roles, research collaborations, design partnerships, and funding discussions.
Start a conversation