Skip to content

Agda-native AI reasoning

agda-native-air builds the infrastructure that lets AI agents work with the Agda proof assistant: a server that exposes Agda's proof state and type-checking verdicts to any agent over the Model Context Protocol, corpora extracted from real libraries, a benchmark of proof obligations with gold solutions, and the measurements of frontier models and of a native proof search on all of it. Agda remains the final arbiter of correctness.

Watch a real session

The demo replays five sessions from the committed archive: a frontier model, the agda-mcp server, and one proof obligation each, with every tool call and every answer on the page in full, beside the 55-row measurement they belong to. Nothing on that page is typed by hand. It is generated from the archive under reports/agent-bench/, and the build refuses to publish it when a number disagrees with the decision record it was checked against.

Read the record

  • The source, the benchmark, the corpora, and the archives are on GitHub. Cite them by their GitHub URL or a Zenodo DOI, not by this site's address: the site is the front door, not the archive.
  • ADR 0002 is the server's design record, and ADR 0001 is proof search on top of it, with the numbers.
  • The documentation for contributors starts at the repository's README.