William DeMeo

Mathematician and formal verification engineer. I work on machine-checked mathematics — proving theorems in dependent type theory, verifying production systems, and building tooling that lets language models work inside a proof assistant.

What I'm working on

Formal verification at IO. Machine-checked specification of the Cardano blockchain ledger in Agda, with the Formal Methods team.

AI tooling for proof assistants. An MCP server exposing Agda's interaction protocol, Claude Skills encoding Agda workflow knowledge, and the agent loops built on top of them.

agda-algebras. A library of universal algebra in Agda, containing a machine-checked proof of Birkhoff's HSP theorem in Martin-Löf type theory.

Background

PhD in mathematics from the University of Hawaii, in universal algebra and lattice theory, under Ralph Freese. 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.

GitHub · Google Scholar · williamdemeo@gmail.com

This site is being rebuilt

It is migrating from a Zola site at williamdemeo.org and an older Octopress site. Publications, talks, teaching, the project portfolio, and the qualifying-exam solutions are still being moved across; the work is tracked in the issue tracker.