Skip to content

AI for formal verification

agda-native-air is infrastructure that lets a language model work inside the Agda proof assistant, and access the same proof-building tools that humans use: load a file, ask what a proof hole needs, try a proof term, query the type-checker.

It has four parts.

  • agda-mcp is a server that exposes Agda's interaction protocol to coding agents as tools.
  • A proof-search loop drives that server to prove theorems by search, with Agda as the only judge of every step.
  • agda-strux extracts whole libraries into structured corpora.
  • A benchmark of proof obligations with committed gold solutions makes every claim about the loop a number others can reproduce.

The hard part was not exposing the checker. It was

making the checker's verdicts trustworthy enough that an agent would use them.

One of the first real sessions with the mcp server plugged in wrote about 1,200 lines of Agda and never called the server, because it couldn't confirm that green meant the whole build would pass.

A second challenging aspect was economics. A batch judgment costs seconds while a question about a loaded file costs milliseconds, so the design must spend batch calls judiciously. This was settled by measurement, and the measurements are below.

Everything on this page is checkable: the repository and its CI, a released corpus with recorded digests, a benchmark whose gold solutions type-check under a pinned toolchain, search runs with identifiers and per-fixture ledgers, nine field sessions written up in both directions, and a research-level theorem formally proved with no hypotheses in the --safe fragment of Agda.

Principal author · 2025– · active
Agda MCP AI tooling

What the server exposes and why it runs Agda in two lanes

agda-mcp is a Haskell server speaking the Model Context Protocol over stdio. It gives an agent thirteen tools for interrogating the proof assistant (Agda 2.8.0):

  • proof-state tools: check_file, get_diagnostics, get_goal, fill_hole;
  • whole-project gate: check_project runs the project's own acceptance command without misreporting its exit code;
  • live queries: type_of, normalize, resolve_name, definition_of, exports_of answer the questions an Emacs user would asks with C-c C-d and friends;
  • corpus query tools: search_by_name, search_by_type, and get_dependencies.

The interaction protocol is the natural surface one wants when constructing a formal proof: a persistent process that loads a file with open holes, reports each goal's type and context, infers the type of expressions that are not in the file, and tests which candidate term can fill a hole.

Exposing Agda as an API in this way enables an agent to use Agda itself for developing Agda proofs rather than engineering inferior tools for understanding contexts and inferring types.

The server runs Agda in two lanes and lets only one of them judge. The batch lane spawns a real agda process per call and derives every verdict from its exit code, never from its prose. The interaction lane keeps one persistent agda --interaction-json child per project root and answers questions about a loaded file in milliseconds; its answers inform and never decide, because interaction-mode Agda loads a file with open holes and succeeds where batch Agda exits 42.

Under both lanes sits one rule: when Agda can answer a question, ask Agda; anything derived from source text is a fallback, never the authority. The measurements that force this shape (disk-warm on a standard-library fixture):

lane cost
batch: spawn agda, read the exit code about 2.6 s per call, paid every call
interaction: keep the file loaded, answer questions 2.6 s once to load, then 1 to 3 ms per question
transport: the round trip and the server's own handling about 6 ms, 0.21 % of oracle time

So verdicts are expensive and unimpeachable, knowledge is cheap and explicitly non-authoritative, and every tool description says which of the two it is.

Every batch verdict echoes, beside success, the exact agda command it is equivalent to and the exit code it was derived from, the binary and arguments that ran, and the project the file resolved to with the libraries Agda received. A get_goal answered from the lane carries the command, the project, and a note of which lane answered, and no verdict at all. A client can check the claim instead of trusting it. Diagnostics come back as data, with Agda's own code for the error, a source range, and the payload the error is about:

{
  "severity": "warning",
  "code": "ModuleDoesntExport",
  "file": "/abs/path/Consumer.agda",
  "range": {"startLine": 20, "startCol": 24, "endLine": 20, "endCol": 50},
  "message": "The module DiagBarrel doesn't export the following:\n  absentName\nwhen scope checking the declaration\n  open import DiagBarrel using (usable; absentName)",
  "involved": {"candidates": ["absentName"]}
}

ADR 0002 records nineteen such decisions, each with the evidence that earned it.

A search loop with Agda as the only judge

A theorem with a hole in its proof is an obligation. The loop keeps the set of open obligations for a file and repeats one move: take the first, propose a handful of candidate terms, and ask Agda through fill_hole whether each type-checks there. An accepted candidate may close the obligation or open sub-obligations, which is how a proof grows. A file is solved only when no obligation remains and a final strict check of the whole file passes; the type that records a solve cannot be built without both. Because a probe costs seconds, the loop optimizes the number of batch judgments and treats everything cheaper as free: judgments are memoized, budgets are counted in probes, and before any probe the loop peeks, asking the lane for the candidate's inferred type with wildcards for its holes and rejecting it if that type cannot match the goal.

On the real obligation stdlib-nat-zero-lt-suc, which imports Data.Nat.Base using (ℕ; zero; suc; _<_; _≤_; z≤n; s≤s) and states

0<1+n : ∀ {n : ℕ} → 0 < suc n
0<1+n = {!!}

the loop runs as follows:

  • check_file on a working copy reports one hole, the initial obligation.
  • get_goal displays it as 1 ≤ suc n, with n : ℕ in context.
  • The proposer offers the closers refl and tt, the assumption n, and applications of the imported names, cheapest first: z≤n bare and (s≤s {!!}) with one hole.
  • The peek keeps s≤s _, whose inferred type suc _m ≤ suc _n can match the goal, and drops n, whose type ℕ cannot, so that probe is never spent.
  • fill_hole refuses refl and tt and accepts (s≤s {!!}), returning one new hole with goal 0 ≤ n; there z≤n survives its peek and is accepted with an empty hole list.
  • A final check_file on the whole file exits 0, and only then is the claim recorded, with the script (s≤s {!!}) ; z≤n.

The searcher never inspected a term's meaning, every hole position came from the server's own list, and the expensive step was gated by everything cheap that could be tried first.

The numbers, and the ceiling they measure

The benchmark has 43 obligations, 22 from the Agda standard library and 21 from agda-algebras, each routine (the term is determined by the goal and the visible context), compositional (two to five known lemmas in a recognizable pattern), or non-obvious (lemmas from outside the immediate context, or an architecture the goal does not determine). Every gold solution type-checks under the pinned toolchain. With the fixed proposal space, the peek on, beam 4, depth 6, and 60 probes per obligation, the record at the current pin (run run-127-repin-full-peek-on-1, byte-stable across four reproductions):

library and tier solved probes wall
stdlib, routine 6/7 22 116 s
stdlib, compositional 0/10 65 239 s
stdlib, non-obvious 0/5 50 173 s
agda-algebras, routine 2/6 11 73 s
agda-algebras, compositional 0/10 43 293 s
agda-algebras, non-obvious 0/5 65 402 s

Eight of 43 in under 22 minutes, and the number is a ceiling, not a shortfall: the six standard-library solves are exactly the six whose gold proofs are single terms expressible from the fixture's own imports, and the other sixteen need an induction, a case split, or a reasoning block, none of which term mode can express. On that tier the peek cut the probe count from 435 to 50 with byte-identical scripts.

Retrieval was measured next. A retrieval proposer widens the pool with corpus lemmas, scoped by what the fixture imports, with the obligation's own original excluded so that the corpus cannot hand the loop its answer. Under that exclusion retrieval added zero solves on either tier, while a labeled control with the exclusion off committed every needle it had removed: 9 of 22 on the standard-library tier, and one wholesale agda-algebras lemma retrieved from a 79-row pool, ranked in the top three, committed in five probes.

The control proves the mechanism; the zero locates the constraint. A single agda-algebras goal draws up to 24,566 raw hits and 3,025 in-scope rows, and a token-overlap ranker drowns the target under the library's generic projections.

Ranking at scale is the measured problem.

The first rung of a learned ranker, an offline recall instrument and a stronger deterministic scorer, is in review at a recall at eight of 9/31 against the placeholder's 1/31, with one more solve on the suite.

Every number above is on the tracking issue with its run identifier, and every retrieval run carries a per-fixture honesty ledger (queries, truncations, hits, in-scope rows, named exclusions, lane rejections, lemmas proposed), so a gamed run and a fair run are distinguishable from the report alone. The decisions are in ADR 0001, explained in the overview.

The corpus underneath

agda-strux runs Agda as a library over a whole codebase and emits one JSON row per definition: name, pretty-printed type, a structural encoding of the type, dependency tokens, and the proof term where there is one. The current release covers the whole of agda-algebras at a pinned commit, 409 modules and 13,123 rows, with the digest confirmed byte-identical across two independent extraction runs and a dataset card recording commit, toolchain, coverage, and license. The benchmark's agda-algebras tier is mined from the same commit, which is what makes the target exclusion above meaningful.

A research-level theorem, proved through the loop

Benchmark obligations are small by construction. The question worth asking is what the tooling looks like on the real thing, a hard, research-level math problem.

The theorem of Kurzweil and Netter says that the class of finite lattices representable as congruence lattices of finite algebras is closed under duals. Kurzweil proved the result in 1985 for a special case (intervals in subgroup lattices) and his student Netter generalized it in 1986, in an article that apparently never appeared, so no published proof exists. It is one of the closure results the finite lattice representation problem rests on, and one my thesis uses as well.

As of September 2026, the theorem is fully formalized and proved in agda-algebras, constructively, under --cubical-compatible --exact-split --safe, with no extra hypotheses, postulates, and instantiated at a certified finite simple group (the alternating group A₅).

The development is eleven literate modules, about 2,000 lines of Agda, in one directory with a narrating barrel, FLRP.KurzweilNetter. Two things in it are new mathematics rather than a port.

  • A no-go theorem. Kurzweil's surjectivity lemma as classically stated, with the partition produced as data, implies excluded middle at level zero: an oracle subgroup above the diagonal decides an arbitrary proposition. The lemma is unprovable as stated in constructive type theory, and the restatement over subgroups with decidable membership is forced. The proof is kurzweilSurjectivity→EM in Interval.
  • A leaner proof. No unary-reduction theorem, which the informal argument cites; a self-contained translation criterion replaces it. No classification of the normal subgroups of Sⁿ as partial products; a family of killed projections replaces it, so every application of simplicity happens in the base group. Formalization pressure produced a strictly smaller dependency graph.

How it was made. The Agda was planned and composed in agent sessions that I directed and reviewed, working through agda-mcp, over three pull requests (#528, #563, #569) between late July and early September 2026, with contemporaneous field reports.

The mathematics follows a manuscript that I have been working on with Ralph Freese and Peter Jipsen, on and off for the past decade. The version of the Kurzweil-Netter theorem appearing in that paper was distilled from lectures that Peter Pálfy's gave on the subject in 2009. The two deviations above were proposed in the AI-assisted sessions and accepted on review.

The sessions' first naming of the result misattributed its history, and that had to be checked by hand against the sources, which is a strong argument for keeping a person in the loop on everything that is not type-checked.

Every session ended with the library's whole-library gate on the command line, never with the server's verdict alone. A companion paper, anchored by the no-go theorem and reporting the AI-assisted workflow as methodology, is proposed to the coauthors.

The workflow knowledge that lives outside the model

The other half of what an agent needs is procedural, and it is encoded in two places. A standing instruction in each client project's agent configuration governs every session that writes Agda there: look for the server's tools before writing anything; plan a module's types and proofs before composing it, and open holes when the goal types are genuinely unknown; the whole-library batch check is the final gate; and field reports are a deliverable, with the explicit instruction for suppressing enthusiasm.

Those reports are the evidence base for this page. Skills are short procedure documents the agent loads when a task matches: diagnosing a slow module (profile before guessing), using the standard library's reflective ring solver and the three places its matching fails, driving the server over its real stdio transport, authoring a benchmark obligation, packaging a corpus with its provenance. Each was written after a session re-derived the procedure the hard way, each records only commands that were run, and they live in a separate agent-configuration repository because they are my workflow, not the projects' product.

What the field record says

Nine sessions between 2026-08-21 and 2026-09-04, in agda-algebras and in the Cardano ledger specification, record the server as a primary development instrument; three more ran without it and say so. Each claim below is falsifiable against the reports.

  • An agent will not use a verdict it cannot check. The July 2026 session that never called the listed server wrote its own post-mortem: a verdict it could not trust cost more than none. The fix was the echo, not a better model, and later reports cite it as what made a cross-worktree verdict trustworthy.
  • A wrong answer is worse than an error. The one agent that reached for the server unprompted sent a relative path, got a bare protocol error, wrote "the MCP agda server crashed", and never called it again. Paths are now resolved against a stated directory and refused by name when they miss.
  • The bugs that matter are trust bugs. Re-verifying the first field report found fill_hole answering ok where agda exits 42, get_goal reporting its own injected macro's type instead of the goal, and hole detection that matched only the literal {!!} while counting tokens in comments. Each let the tool lie to the model, and each was fixed before any ergonomic work.
  • Hole-driven development was mostly unused, rightly. The dominant tool across the nine sessions was check_file; the goal and fill tools appear in one. When an agent can read the sources into context and design the proof whole, write-then-check wins; holes pay when the goal types are unknown. Reading substitutes for asking up to a ceiling the library is now crossing, which is the case for retrieval.
  • The value was latency, structured diagnostics, and the echo, not capability the shell lacks. Warm check_file rounds ran 2 to 35 s against 20 s to 10 min for the shell, which stayed better for per-file sweeps and the final gate; the reports say so each time it was true.
  • An agent's time goes to discovery, not invention. An audit of one session found most of it spent finding what the library already had and what it was called, with more such questions than proof obligations. The agent knows the type, not the name, so text search cannot answer them; that audit is why retrieval as a server tool comes next.

What a typechecker's feedback makes possible

All of the above rests on one property of the domain. The reward signal is dense: every candidate at every hole is judged, and a failed run says why it stopped.

It is unfakeable: the verdict is an exit code from a process that does not read the agent's summary of its own work, so neither an agent nor a benchmark can talk itself into "probably green". And it is cheap in the right lane, so a loop can ask many questions per judgment and the number of judgments becomes the only cost worth optimizing.

The consequence is that negative results are as usable as positive ones: a zero with a control, a ledger naming every exclusion, and a ceiling stated as the finding let the next experiment be designed rather than guessed at. Domains without a checker cannot say any of this.

Artifacts

The repository, the corpus, the benchmark, the field reports, and the agda-algebras development are public. The agent configuration is kept separately, and the second client project is the public Cardano ledger specification.

What's next

The numbers are small and the ceilings are stated. In the order the record argues for:

  • retrieval as a server tool, scope-aware and type-directed, answered through the checker, so that "is there a term of this type in scope here" is one call;
  • ranking at scale, the hand-off to a learned premise-selection model, evaluated against the recall instrument and the ledgers rather than solve counts alone;
  • past the term-mode ceiling, since sixteen of the 22 standard-library obligations need induction, a case split, or a reasoning block, and expressing those without giving up Agda as the only judge is the open design question;
  • the server as a daily instrument, nine ergonomic follow-ups from the field record;
  • a replay on this page, a recorded session annotated beat by beat, which this page should embed and does not yet.

The thread runs back to agda-algebras: 60,000 lines of type-checked, human-written Agda with a published theorem at the center, and now a research-level theorem proved through this tooling, is a rare thing to have, and what it is rare for is exactly this.