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 library of universal algebra in Agda, containing 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
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 formal methods production
Universal algebra and lattice theory
The mathematics the rest of this rests on: congruence lattices of finite algebras and the finite lattice representation problem, and later work on the algebraic approach to constraint satisfaction.
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