Projects¶
Machine-checked mathematics, formal verification at production scale, and tooling that lets language models work inside a proof assistant.
Ordered by relevance to what I work on now, not by date.
Tooling that lets language models work inside a proof assistant: an MCP server exposing Agda's interaction protocol, a semantic training-data extractor, Claude Skills encoding Agda workflow knowledge, and the agent loops built on them.
Agda MCP AI tooling
A formalization of universal algebra in Agda, built as a substrate for research in the subject; its flagship result is the first constructive, machine-checked proof of Birkhoff's HSP theorem in Martin-Löf type theory, joint with Jacques Carette.
Agda type theory universal algebra setoids
The Cardano ledger specification
Machine-checked specification of the Cardano blockchain ledger in Agda, written with the Formal Methods team at IO — a specification that has to track a system under active development and produce artifacts the rest of the organization consumes.
Agda Haskell formal methods production
Universal algebra and lattice theory
The finite lattice representation problem, open since the 1960s: my thesis settled every lattice with at most seven elements but one and introduced the methods that did it. With the later work on the complexity of constraint satisfaction, and a machine-checked revival now under way.
universal algebra lattice theory complexity
Category theory: a concise course
An online course in category theory, coauthored with Venanzio Capretta and Charlotte Aten, built out from Capretta's notes for a short course at the Midlands Graduate School.
category theory exposition