Independent researcher · formal methods and systems
Small, machine-checked abstractions for AI reliability, tied to real runtimes.
Most of my work is a rulebook proved in Lean 4 and a thin engineering layer that makes the proof matter in production: conformance tests, receipts, demos, and honest non-claims. Formal methods with deployment instincts. The recurring question is the same one every time, do these observations carry enough to justify this claim?
A verified mediation layer for agent tool use over MCP. A default-deny gate whose non-bypass is proved in Lean, so an agent can read and reason but every protected effect is forced through an exact, recorded, checkable approval boundary. It emits replayable decision receipts, not vibes. It enforces authorization at the effect boundary; it does not claim to read intent.
A Lean 4 / Mathlib formalisation of what a single-layer hard-attention model can compute over Boolean cubes. Single-head outputs are exactly decision lists; head-count lower bounds become witness-number lower bounds. Headline: k(maj₅) = 4 exactly, majority-of-five provably needs four attention heads, one above its certificate complexity of three, the first proven gap of its kind. Kernel-clean on {propext, Classical.choice, Quot.sound}, no sorry, no native_decide in the structural proofs.
A verified, embeddable, eventually-consistent distributed event log. Machine-checked strong eventual consistency and convergence under drop, duplication, and reorder, so anything built on top gets convergence for free. Aimed at load-bearing-integrity work over dirty networks: cold-chain, custody, offline-first sync.
A family of small Lean 4 developments, each narrowing a load-bearing claim in optimisation, dynamics, consensus, or learning to a theorem the kernel will actually check, with its axiom footprint left visible and its non-claims named. Gradient descent, Kuramoto synchronisation, CRDT convergence, LTL enforcement, PAC bounds, and more, indexed in one place.