William DeMeo · formal verification × AI
Mathematics, machine-checked.¶
Formal proofs & production systems in Agda; AI research & development; language models driving proof assistants, with type-checker as reward signal.
Counted, not asserted: the figures are from ualib/agda-algebras at 4662373 (2026-09-06). 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¶
A MCP server exposing Agda's interaction protocol to language models and a semantic extractor for training and proof search.
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, 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
- Agda modules
- 339
- postulates
- 0
- venue
- TYPES 2021
agda-algebras.universalalgebra.org · captured 2026-09-12
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
- 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, 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
- PhD thesis
- University of Hawaii at Manoa, 2012
- arXiv
- 1204.4305
First page · arxiv.org · captured 2026-09-12
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. Research tells that story in full.
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 · ORCID · Google Scholar · arXiv · DBLP · Semantic Scholar · Publications · Contact
This site is still being rebuilt
Content is migrating here from the two sites this address used to serve — a Zola site, and an older Octopress one. The publications, the projects, the research narrative, and the blog have landed; talks, teaching, and the graduate qualifying-exam solutions have not. Every URL either of them served still resolves.