Trend Watch: Agent Work Is Starting to Arrive With a Proof Attached

When an agent writes more than anyone can review, someone has to decide what counts as evidence that the work is correct. This week's research points to an answer: separate the author from the checker, and make the check mechanical wherever possible.

Four examples of the same arrangement

Mathematics. DeepMind's "Fan Factories" reports "a two-agent AI harness: one model generated the proofs, and a second model verified them", with the algebraic identities and feasibility witnesses machine-checked in Lean 4.
Software. Microsoft Research's PDD Kit, described on November 5, turns a developer's intent into a formal specification in Verus and proves that agent-written Rust meets it. In a roughly 5,000-line storefront, the team verified the login logic and uncovered existing bugs, and the developer "never read the generated code line-by-line".
Scoring. TB-MathModel, covered here yesterday, gives zero to an answer that fails a programmatic gate or its 624 Lean 4 obligations, so a plausible but impossible answer earns nothing.
Self-improvement. Flex-RSI, posted November 6, keeps an agent's new solution only "if it scores higher on held-out validation data", so the agent revising its own harness cannot award itself the gain.

What a proof does not cover

The arrangement is useful because its limits can be stated. PDD Kit is careful about this: it labels every result as proof or as evidence, and says "A passing test only shows the code worked on the inputs it tried". It also asks the developer to sign off on the trusted computing base, the code a proof assumes behaves as described. A verified login is verified only against its specification, and a wrong specification yields a correct proof of the wrong thing.

The DeepMind papers show the same boundary. The Lean checks cover algebraic identities, while the complexity results still rest on the standard heuristics of number field sieve analysis. In the companion experiment, a 32-bit index overflow made the first computed root wrong, and it had to be tracked down and fixed during the run. Formal checking did not make the engineering safe by itself, and a supervisor model still had to audit the results.

There is also a cost that benchmarks do not show. Writing a useful specification is skilled work, and the process moves human effort from reading code to deciding what the code must never do. That may be a better use of a reviewer's time, but it is not free.

What remains uncertain. These are four examples selected because they share a pattern. PDD Kit's published case covers login logic in one application built by its authors. We have not seen independent data on how often specifications written with agent help are wrong, or whether teams keep them current as code changes.

Analysis: The pattern can be adopted well short of formal methods. At Belgavi's Book Store, Hansini could start with one rule worth proving or exhaustively testing, such as a refund never exceeding what was paid on the order, kept in a check the coding agent cannot edit. Have a different model or a plain script judge the result, and record which claims are proved, which are tested and which are simply trusted. The value of the arrangement lies in knowing which of those three you are relying on.

Sources and evidence

Agent work is increasingly checked by something other than its author: DeepMind's model-verified, Lean-checked factoring results, PDD Kit's Verus proofs of agent-written login code, TB-MathModel's feasibility gates and Flex-RSI's held-out validation. Proofs only cover the specification and its assumptions. Separate author from checker, and record what is proved, what is tested and what is trusted.