Projects
Systems I build and contribute to. Most of them are attempts at the same question: how much of a proof can a machine work out on its own, and how do we stay sure the answer is right?
Sketchpad
Autoformalisation · Isabelle and Lean · University of Edinburgh
Sketchpad turns natural-language proofs into structured formal sketches for practitioners working in Isabelle and Lean. Rather than treating a proof as one monolithic translation problem, it uses a graph-based representation that decomposes a proof into individual statements — which makes fine-grained autoformalisation possible and lets the system work usefully with partial or incomplete proofs.
The project is supported by Renaissance Philanthropy’s AI for Math Fund, joint with Wenda Li at Edinburgh.
Lemmanaid
Lemma conjecturing · Isabelle
Useful intermediate lemmas are normally something a human has to think of. Lemmanaid automates that step by splitting it in two: a fine-tuned language model proposes a lemma template describing the shape a lemma should take, and symbolic methods fill in the details. The neuro-symbolic split is what makes it work — neither half is strong enough alone.
Evaluated across formal mathematics libraries, it recovers a substantial fraction of human-written reference lemmas, and outperforms frontier language models used directly on the same task.
Paper · Earlier workshop paper
Proverbot9001
Proof automation · Rocq
Proverbot9001 uses neural networks to synthesise correctness proofs for software, searching the space of proof scripts in Rocq with a learned model guiding which tactic to try next. It was, at publication, able to prove a significantly larger share of theorems in a real verification benchmark than prior automated approaches.
VeriWasm
Verification · WebAssembly
WebAssembly promises memory isolation, but that promise is only as good as the compiler that lowers it to native code. VeriWasm is a static offline verifier that checks the safety of natively-compiled Wasm binaries directly, so you no longer have to trust the compiler to have got sandboxing right. It found real isolation bugs in a production Wasm compiler.