CASE STUDIES
Worked examples — open and checkable
Evidence you can open and run, not claims: an open-source Rust crate that runs its proof in your browser, and a live production trust platform built end to end.
OPEN SOURCE
bitrep — any order, any hardware, same bits
An open-source Rust crate for order-invariant, bit-identical floating-point reductions: exact mergeable sums whose bytes are identical on every architecture — proved in Lean, checked by Kani, fuzzed against an oracle, and asserted across x86-64, ARM64, Windows and WebAssembly by one SHA-256 in CI on every commit.
PRODUCT ENGINEERING
Shipped, full-stack
A live production system built end-to-end — auth, data, authorization, compliance, deployment.
A system that needs to prove itself?
These are examples of the work — verifiable systems whose outputs carry a proof anyone can reproduce. Open to roles, research collaborations, and partnerships.
Start a conversation