About

I research how to bring formal methods into the world of AI-generated code. The long-term vision is what people call veri-coding: a future where every function an LLM writes comes with a machine-checked proof of its correctness. We're not there yet, but that's the direction.

I contract with the Beneficial AI Foundation as a Senior Research Scientist, contributing to Signal Shot, a large-scale effort to formally verify the Signal protocol and app in Lean. My focus is post-quantum cryptography formalisation in the secure-messaging project, where we build machine-checked specifications and proofs for secure messaging protocols.

Separately, I contract with Kodamai as an AI engineer, building verified agentic infrastructure for fleets of specialised enterprise agents. My work uses applied category theory and type theory to give structure and guarantees to multi-agent systems, alongside neuro-symbolic AI.

My background is in pure mathematics. I have a PhD in Algebraic Geometry. That training in rigorous abstract reasoning turns out to be useful when you're trying to make AI systems you can actually trust.