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
- CI
- passing · 7fceca3
- last commit
- 2026-09-10
github.com/formalverification/agda-native-air · captured 2026-09-13
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
- Agda modules
- 339
- postulates
- 0
- venue
- TYPES 2021
agda-algebras.universalalgebra.org · captured 2026-09-12
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
- venue
- FMBC 2024
- DOI
- 10.4230/OASIcs.FMBC.2024.2
intersectmbo.github.io/formal-ledger-specifications/site · captured 2026-09-13
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
- PhD thesis
- University of Hawaii at Manoa, 2012
- arXiv
- 1204.4305
First page · arxiv.org · captured 2026-09-12
Forty-three University of Hawaii graduate qualifying examination papers in algebra and analysis, 1991 to 2008, with worked solutions written as one cross-referenced document; the problems are the department's, the solutions are mine, and the Agda formalization they are being prepared for has not started.
real analysis complex analysis algebra
formalverification.io/exams · captured 2026-09-12
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
categorytheory.gitlab.io · captured 2026-09-12
Other work¶
Smaller projects, tools and contributions; the ones that have stopped moving say so.
-
fin-lat-rep: the working repository behind an article on representing small lattices as congruence lattices of finite algebras, with Ralph Freese and Peter Jipsen: the LaTeX source, the lattice lists, and the programs that searched them.
-
lean4crypto: a machine-checked proof in Lean that the one-time pad achieves perfect secrecy, with the notes behind it.
-
claude-tooling: one versioned source of truth for my Claude Code configuration, global and per-project, installed by symlink so that a fresh machine is a clone and one
make install. -
github-project: keeps a repository's roadmap in one Markdown file and syncs it with GitHub's issues and milestones in both directions.
-
agda-lagda-migrator: converts LaTeX-literate Agda to the Markdown-literate form GitHub and MkDocs render, without disturbing layout-sensitive code.
-
universalalgebra.org: an expository site on the finite lattice representation problem, its history and where it stands.
-
Overalgebras: the GAP programs behind a 2013 Algebra Universalis paper on expanding finite algebras to control their congruence lattices.
archived -
The Universal Algebra Calculator: Ralph Freese's calculator for finite algebras; I wrote its command-line interface and six merged pull requests to its source.
dormant