William DeMeo · formal verification × AI
Mathematics, machine-checked.¶
Proofs and production systems in Agda — and tooling that lets language models drive the proof assistant, with the typechecker as the reward signal.
Counted, not asserted: the library figures are from ualib/agda-algebras at 594bc1c (2026-08-01), the request count from this site's own audit. Hover a figure for the command that produced it; make evidence recounts.
Mathematician by training with a PhD in universal algebra and lattice theory; formal verification engineer by trade. I work on machine-checked mathematics: proofs and production systems in Agda, and tooling that lets language models work inside a proof assistant.
What I'm working on now (2026). The machine-checked specification of the Cardano ledger in Agda, with the Formal Methods team at IO, and agda-native-air, making Agda's interaction protocol accessible to language models so they can interact with the proof assistant the way humans do, rather than merely type-checking complete proofs.
Featured projects¶
An MCP server exposing Agda's interaction protocol to language models, and the agent loops built on it.
Agda MCP AI tooling
A formalization of universal algebra in Agda, and a substrate for research in it; the flagship result is a constructive, machine-checked proof of Birkhoff's HSP theorem in Martin-Löf type theory.
Agda type theory universal algebra setoids
The Cardano ledger specification
Formal methods at production scale: an Agda specification that must track a system under active development.
Agda Haskell formal methods production
Universal algebra and lattice theory
The finite lattice representation problem, open since the 1960s, and the algebraic approach to the complexity of constraint satisfaction. A thesis result, and a machine-checked revival now under way.
universal algebra lattice theory complexity
The through-line across all four is an interest in what is mechanizable: which structures admit effective procedures, and what it takes to make an argument checkable by a machine rather than by a referee.
The full set is in Projects.
Recent writing¶
- Congruences of Partial Algebras · April 6, 2017
- 3-SAT and Partition Lattices · January 11, 2015
- A Problem of Pálfy and Saxl · February 13, 2014
More in the blog.
Elsewhere¶
Before moving into industry I held research and teaching appointments at Charles University in Prague, the University of Colorado Boulder, the University of Hawaii, Iowa State University, and the University of South Carolina. The CV has the full record and about has the longer version.
Email · GitHub · Google Scholar · ORCID · arXiv · Publications · Contact
This site is still being rebuilt
Content is migrating here from a Zola site at williamdemeo.org and an older Octopress site. The publications, the projects, and the blog have landed; talks, teaching, a research narrative, and the graduate qualifying-exam solutions have not. Progress is tracked in the issue tracker.