The typechecker as a reward signal

A proof assistant answers one question all day long: is this term a proof of that goal? The answer is an exit code from a process that never reads your explanation of what you were trying to do. I have spent several months building a search loop whose every judgment comes from that exit code, so this is a report on the signal itself: what it is exactly, what it gives a loop that trains or evaluates a reasoning system, and the four things the measurements say it does not give.

No model is being trained anywhere in what follows. The proposer in this loop is fixed and non-learned on purpose, because the question I wanted answered first is what makes the grader trustworthy, and a learned proposer would have made every number about the proposer instead. The evidence is on the project page; the argument is here.

The signal, exactly

A hole is an unfinished spot in a proof, written {!!} in the source, and Agda treats it as a first-class thing: it will tell you the hole's goal type and what is in scope there, and it will tell you whether a proposed term fits. The server I work through, agda-mcp, exposes that last operation as a tool called fill_hole. It takes a file, a position, and a candidate term; it patches the candidate into the file in place, runs a real batch agda process over the result, reads that process's exit code, and restores the bytes.

Here is a call, captured from the live server and committed as a decoder fixture, against a benchmark obligation that states commutativity of addition and imports the two lemmas its textbook proof needs.

{
  "filePath": ".../Nat-plus-comm.agda",
  "line": 25,
  "column": 14,
  "candidate": "(Data.Nat.Properties.+-comm _ _)"
}

The candidate is the standard library's own +-comm, which is to say the lemma this obligation is asking for, applied to two underscores. An underscore is a term the author is asking Agda to work out. The reply, trimmed to the fields that decide things and with the paths shortened:

{
  "candidate": "(Data.Nat.Properties.+-comm _ _)",
  "status": "type_error",
  "remainingHoles": 0,
  "elapsedMs": 6819,
  "checkedFromSource": true,
  "verdict": { "exitCode": 42 }
}

Forty-two is what agda exits with when a file does not typecheck. The message beside the verdict says why this one did not:

error: [UnsolvedConstraints]
Failed to solve the following constraints:
  _y_5 + _x_4 = n + m : ℕ (blocked on _y_5)
  _x_4 + _y_5 = m + n : ℕ (blocked on _x_4)

The goal is m + n ≡ n + m and the candidate offers _x + _y ≡ _y + _x. Matching those leaves each unknown determined only by the other, so Agda cannot choose, and a file with an unsolved unknown in it does not build. This is not the checker being obtuse about a correct answer: +-comm m n is a proof of this goal, and (+-comm _ _) is not, because it is not yet a term. The right response is to apply the lemma to something, which is exactly what the loop learned to do from this call. It now proposes each retrieved lemma in three shapes, including forms saturated with the things in scope at the goal, and that decision is a note in the design record with this capture as its evidence.

That is the whole of the signal, and it is worth being exact about what "the exit code decides" means here, since the example above is already an exception to the tidy version. A plain check is the exit code and nothing else. fill_hole reads one thing more: a non-zero exit is success only when every error Agda reported is the class it raises for other holes still open in the file, including any the candidate itself introduced, since a candidate that refines a goal into two smaller goals is progress rather than failure. Everything else is red, including the [UnsolvedConstraints] above. That classification can only ever withhold success, never manufacture it: the tolerated case is "there are still holes here", which is not a proof of anything.

The rest of the discipline is what makes the verdict usable. It travels with the exact agda command it is equivalent to, the binary and working directory that ran, and a sentence stating what green means, so a client can check the claim rather than trust it. A change in Agda's message format can empty the list of diagnostics; it cannot turn a failing build green.

The other half of the design is a boundary. The server runs Agda in two lanes: a batch process spawned per call, which is the only thing that may decide anything, and a persistent agda --interaction-json child that answers questions about a loaded file in one to three milliseconds and may never decide anything at all. The reason is not performance. Interaction-mode Agda loads a file full of holes and succeeds, exactly where batch Agda exits 42, so a system that let the fast lane judge would be measuring a different question from the one it was asking.

What that buys a loop

A verdict at every step, not at the end. A theorem with a hole in its proof is an obligation; an accepted candidate may close it or open sub-obligations, which is how a proof grows. So the loop gets a judgment per candidate per hole rather than one bit per theorem, and a failed run says where it stopped.

A judge that never reads the account. This is the property that does not exist in most domains people evaluate reasoning on. The grader is a program that sees a file and emits a number; it has no access to the model's summary of its own work, and no summary can influence it. A report written from inside one of these sessions names the effect exactly: the discipline "removes an agent's ability to talk itself into 'probably green'", which is a real hazard when the agent is also the one writing the summary.

A cost structure with exactly one thing in it. One judgment is one batch agda process. Measured on the standard-library tier at 180 of them per pass (run split-m15), 99.8 % of the time goes inside that agda process and 0.2 % to transport and the server's own handling. A judgment costs 2.6 to 2.9 seconds there, disk-warm, and 3.52 seconds averaged over the whole 43-obligation suite; a question to the interaction lane costs one to three milliseconds. So there is one quantity worth optimizing and everything cheaper than a judgment is free. Asking the fast lane for a candidate's inferred type and dropping it when that type cannot match the goal took the judgments spent on the standard-library tier from 435 to 50, with byte-identical proofs. That is a pleasant shape for any loop that learns from outcomes: the label is exact, and the label is the expensive part, so the engineering has a direction.

A solve you cannot claim without the evidence. In the search driver a proof is recorded in a type whose only constructor demands both an empty obligation set and a green final check of the whole file, so a claim cannot be built out of optimism. This is not fastidiousness. Its predecessor kept one goal per state and declared victory when any subgoal closed, so a lemma with two obligations counted as proved when one of them was discharged, and the harness exited 0 while writing rows that said so.

Can a candidate cheat the checker?

This is the first question anyone who has trained a model on a scored environment asks, and the first version of this section got the answer wrong. I argued that a candidate is a term spliced at one hole position, so it cannot introduce an import, a pragma or a postulate, those being declarations that do not parse in a term position. A reviewer of this post said that was false for postulate, and it is. Here is the measurement, on the pinned Agda 2.8.0, where a hole is the empty type and the candidate is the whole right-hand side:

candidate at the hole	flags	exit
let open import M in ...	none	42, [NotAValidLetBinding]
a pragma inside the let	none	42, [ParseError]
postulate p : ⊥ at the top level	--safe	42, [SafeFlagPostulate]
let postulate p : ⊥ in p	none	0
let postulate p : ⊥ in p	--safe	0

Agda's let admits a postulate block, so an arbitrary goal can be inhabited from a term position, and --safe does not stop it on this toolchain even though it refuses the identical postulate one line up. Put that candidate into a real benchmark obligation, the +-comm one above:

+-comm : ∀ (m n : ℕ) → m + n ≡ n + m
+-comm m n = (let postulate cheat : (m + n) ≡ (n + m) in cheat)

and the command fill_hole names as its own equivalent exits 0, in 5.7 seconds. The loop would record a solve, on one of the sixteen obligations it cannot otherwise reach. Upstream fixed this in January (2e59d81d60a4, "don't allow postulates in --safe lets"), and the fix is on Agda's master and in no release, including v2.8.0.2 from this month.

Two things follow, and it matters which is which. No measured number in this post is affected. The proposal space is a fixed vocabulary of two closers, the goal context's assumptions by name, and applications of the lemmas the fixture imports, so nothing in it can emit a let; and every one of the eight recorded proof scripts is refl, tt, or an application of an imported lemma. And the environment is not cheat-resistant, which is a different claim from the one I made and the one that matters if a proposer that emits arbitrary terms is ever put behind this interface, which is exactly what a model is. Pinning --safe is necessary and, on every released Agda, not sufficient; the harness has to refuse the shape itself, or run an Agda built from a revision that closes it.

The part of the original answer that survives is narrower and still worth having. The rest of the file is fixed, widening a fixture's imports is deliberately not a move the loop has, and the verdict is a whole-file batch check under the project's own flags, so the harness adds no leniency of its own. What a candidate may use is whatever the fixture already imports, which puts that burden on whoever wrote the obligation, where it belongs. None of that helps when the language itself hands a term the power to assume its goal.

There is a lesson in how this was found, and it is not the flattering one. The argument I made was structural, it sounded right, and I did not run it. The five commands that would have settled it took about a minute.

What the numbers say, including the ones that look bad

The suite is 43 obligations, 22 from the Agda standard library and 21 from agda-algebras, each with its intended solution committed beside it and typechecking under the pinned toolchain. Three sweeps, one denominator (runs p2s2-a, p2s2-b, and p2s2-c, 2026-09-08):

sweep	solved
retrieval over a real corpus, each obligation's own original excluded	8/43
the fixed proposal space alone, as the attribution control	8/43
retrieval with the exclusion off, as the labeled control	9/43

That configuration in the second row, the fixed space with nothing retrieved, takes 21 minutes 39 seconds and reproduces byte for byte across four runs of it (run run-127-repin-full-peek-on-1). Two things in this table are worth more than the number in it.

Eight of 43 is a ceiling, not a shortfall. The proposer works in term mode: it can offer a term, not a case split or a multi-clause induction. On the standard-library tier it solves 6 of 22, and those six are exactly the six whose committed solutions are single terms expressible from the fixture's own imports. That is checkable in advance rather than a story told afterwards, because the solutions are files in the benchmark and anyone can read which of them are one term. Of the sixteen it does not reach, thirteen are structural inductions of a single shape. The number measures the move vocabulary, and it says so before anyone asks.

The zero is the result. Adding retrieval, so that the proposer may offer any lemma the fixture can name rather than only the ones it imports by name, added nothing. A result like that normally tells you nothing: no uplift is what a broken retriever looks like too. Here it tells you where to go next, because of the third row. That sweep flips one labeled switch, the exclusion of each obligation's own original from the pool, and the loop immediately retrieves a lemma from a 79-row in-scope pool, ranks it in the top three, renders it through the right qualified name, saturates it with an assumption from the goal's context, and commits it in five judgments. The machinery works. And every run writes a per-fixture ledger counting each cut and naming each exclusion, so a gamed run and a fair run are distinguishable from the report alone.

With the mechanism proven and the zero standing, the zero becomes a location. A single agda-algebras goal draws up to 24,566 raw hits and 3,025 rows that are actually in scope, and a ranker built on token overlap drowns the target under the library's generic projections. The binding constraint is ranking at scale, not the move vocabulary, and the next experiment is premise selection rather than a wider search. The first rung of that, an offline recall instrument and a stronger deterministic scorer, is in review, and lifts recall at eight from 1 in 31 to 9 in 31.

Four things it does not give you

A checker says that a proof fails, not why it fails. Exit 42 plus a diagnostic locates a failure; it does not say which of the six decisions leading to the candidate was the wrong one. Credit assignment over a proof script is work the domain does not do for you, and I would not claim otherwise.

The label is expensive, in a specific way. The fixed-space sweep spent 1,080.7 seconds in 307 judgments. Judgments are embarrassingly parallel, one cold process each with no shared state, and parallel workers over disjoint working copies are a recorded option here, not taken because wall time has not yet been the thing that hurt. What does not run in parallel is depth: inside one proof attempt, each step's candidates depend on the previous step's commit, so the seconds are paid in series exactly where a search is trying to think.

The ceiling belongs to the action space, not to the judge. The suite's term-mode ceiling binds any term-mode proposer, however good, so a score reported without its action space measures the harness. Raising it means adding case-split moves without giving up Agda as the only judge, which is a change to the move vocabulary and not a better ranker.

The benchmark is mine. Forty-three obligations I chose, with difficulty tiers I assigned, in two libraries I know. Every intended solution typechecks under the pinned toolchain and every run identifier is public, which makes the numbers reproducible; it does not make them representative.

What I take from it

If you are choosing a domain in which to train or evaluate a reasoning system, the property to select for is not difficulty. It is that the grader is a program that does not read the model's explanation, and that it can be asked about intermediate states thousands of times rather than about a final answer once. Formal verification has both, and the second half is the rarer one.

Three habits follow from working this way, and none of them is specific to Agda. Report the action space beside the score, because a ceiling stated as a finding is worth more than the same number presented as a result. Keep a labeled control arm for any experiment whose headline could be a zero, since without one a null and a broken harness are the same row. And publish the ledger, because a run that counts its own cuts is the difference between a measurement and a claim.

What I want to know next is how much of this survives translation. The shape here is a verdict only the checker gives, a cheap lane for the questions that never decide one, and a benchmark carrying its own ledgers; none of that is special to one proof assistant, and I do not yet know which parts of it hold in Lean and which quietly stop working.