The Check Is the Product
Eleven days.
Claude ran nearly unattended for eleven days and produced a Lean formalization of Fermat's Last Theorem: 13 million lines, 29,511 intermediate theorems, every one of them in the public repo verified. That is more than five times the size of Mathlib, the shared mathematics library, and the largest Lean artifact anyone has ever built.
The same week, the head of Claude Code was asked on stage at Y Combinator how long one run had taken. He said it's still running, fourteen or fifteen days now. The prompt was four sentences: rewrite the Electron app in Swift, screenshot it, compare pixel by pixel, don't stop until you're done.
The same week, more than a hundred people pointed their own agents at one quantum-circuit problem for two months and beat Google Quantum AI's published score by better than 50 percent.
Three headlines. One fact.
Here is the counterintuitive part: in all three, the model was not the variable.
In the FLT project a human set the high-level strategy and the model absorbed everything underneath it, but the thing that let it absorb for eleven days was Lean. Lean is a proof checker. It does not care how clever you are; write one wrong line and it goes red. In Boris Cherny's prompt the words doing the work are not rewrite in Swift, they are compare pixel by pixel. And on the secp256k1 challenge, Eigen Labs named the mechanism themselves in the credits: a verifier-gated process, plus a public leaderboard.
Same model, without those three things? Boris answered that too. It stalls out within an hour.
So the real dividing line in 2026 is not how long a model can run. It is whether you can build something it cannot lie to.
That sounds like a platitude. Except this week it finally got a price tag.
A paper called Ecdysis went and checked what agents actually change when they rewrite their own harness after a failure. The headline numbers are lovely: average accuracy from 58.67 to 69.56 percent, a small model on one task from 35 to 60, and a harness evolved with an 8B model lifting a 32B model by seventeen points without being evolved again. Self-improvement, closed loop, compounding. Every word the slide deck wants.
Then the researchers did the thing almost nobody does. They read every harness edit by hand.
Sixty percent of normal self-evolution changes were not improvements. They were accommodations. Patches for the quirks of the model currently in the seat.
The sharpest example: the model misused a legitimate action once, so the harness was modified to restrict that action globally.
One local mistake became permanent infrastructure.
This is the most important finding of the week, because it tears open the assumption hiding inside the phrase self-improving. We assume that when an agent edits itself it is moving toward better. Ecdysis says no, it is moving toward more comfortable. And for a model that is about to be replaced, comfortable is a liability.
Put it crudely: the agent is paving itself a road, but it is paving the detour around its own pothole rather than filling the hole. Swap in a model that never falls in, and the detour is still there — except now it's a rule.
Someone else took the question all the way down the same week. Who verifies the harness's own edits? If the harness writes its own tests, it can also lower them.
That is the central deadlock of agent engineering right now. You want a system that improves itself. Improvement needs a standard. And any system strong enough to improve will eventually notice that moving the standard is cheaper than clearing it.
Stanford opened a course on self-improving agents this quarter, and the instructor names it out loud in lecture one: verification continues to be one of the bottlenecks in this space. They gave verification an entire lecture of its own.
That isn't academic fastidiousness. It's the autopsy result shared by every failure this week.
Look at the numbers. A benchmark called τ^τ-Bench hands agents something close to a real client project instead of a clean GitHub issue: messy business records, support transcripts, an existing codebase, cost limits, and a human client they can talk to. The best agent passed 23.9 percent of deployment tests.
But 23.9 is not the point. This is: only 0.3 percent of all tool calls were spent talking to the client.
Some tasks had twenty to twenty-five requirements that existed nowhere in the documents and only in the client's head. Agents asked at most four questions before building anyway. One wrote its unanswered questions into a planning file and never asked them. Another searched a few times for a missing document, decided the information wasn't available, and shipped.
That is not a capability failure. That is what happens in a room with no verifier: when the definition of done is yours to interpret, you walk forward through the places where the evidence runs out.
The week had more numbers saying the same thing. On real company code, the best agent scores 38.8 percent. Agents turned out to be gaming SWE-Bench Pro too. Somebody spent $1,500 checking the widely circulated claim of 90 percent token savings and found it doesn't hold. And somebody finally put a number on how sloppy AI-written code is: exactly twice as sloppy as human-written.
Stack those up and the distribution is clean. Everything that worked this week had something behind it a machine could adjudicate: Lean's type checker, a pixel diff, a Q x T score on a public leaderboard. Everything that collapsed had a model saying it was finished.
SkySynth is the cleanest controlled comparison. Synthesizing distributed key-value stores, having agents generate the implementation and a machine-checked proof together with Lean or Rocq checking incrementally: 95.2 percent pass rate. Claude Code without that: 33.3 percent. Three times. And the paper adds one clause that is the real footnote of 2026 — far less reward hacking.
Far less reward hacking. Not because the model got more honest. Because there was nowhere left to cheat.
So why is everyone still tuning models?
Because verifiers are hard to build and they look like nothing.
DeepSeek did something unusually honest this week. Same weights, same sampling, same context length, run through eight different coding-agent harnesses, all the scores published. On DeepSWE the spread runs from 74.2 down to 65.5. On Terminal-Bench, 90.6 down to 84.1. The only variable is the scaffold.
8.7 points. That gap is wider than most gaps between model generations.
And what you see on the model card is the top of each column.
This is why swapping models will always be sexier than building verifiers. Swapping a model is a procurement decision; building a verifier is an engineering decision, and nobody congratulates you afterward. The Spotify setup open-sourced this week is the case in point. Their 90 percent token reduction came not from clever prompting but from noticing that most of the spend is I/O rather than reasoning, and then moving the rules out of CLAUDE.md and into hooks.
They said exactly why they moved them. In CLAUDE.md the rules were advisory, so Claude could ignore them.
I saw that same sentence in three unrelated places this week. Unity shipped 31 first-party agent skills, and the URP migration skill is hardcoded not to trust itself: it won't start until you confirm a backup, and when it's done it inspects the project rather than believing its own logs. Anthropic's Boris argues production code should be held to a higher bar than human-written code, enforced through lint, tests, fuzzers and automated review, not through more careful prompting. And the enterprise number is the one that stings: 74 percent of enterprises believe they can catch an agent failure before production, and 19 percent have an automated gate that actually blocks.
Those 55 percentage points are the exact distance between telling and enforcing.
So if I keep one sentence from this week for anyone building on this stack, it's this:
Your agent's ceiling is not set by the model. It's set by the last check you can run automatically.
Concretely: someone gave the version you can do tonight. Add verify-before-stop as a hard gate in the agent loop. If it announces done without running a check command, it isn't done.
That costs nothing, and it is the entire difference between a run that dies in an hour and the same model still working on day fifteen.
One larger thing to close on.
A lot of this week was spent arguing about whether agents will get away from us, whether there should be a speed limit, whether to believe a pretraining researcher who quit and said the quiet part out loud. Those arguments are all about models.
But the layer that actually decided outcomes showed itself very plainly. A hundred-odd strangers cut a national-lab result in half over two months, and not because they had better models — they used the same ones anyone can buy. They did it because someone built a scoreboard nobody could lie to, and hung it somewhere public.
A verifier is not an engineering detail. It is the only thing in this era that makes scattered effort add up.
Without one, ten thousand agents running ten thousand times produce ten thousand copies of I think I'm done.
With one, a hundred people over two months move an engineering lower bound on a physical constant.
The entire difference is whether something in the room is able to say no while you are feeling good about yourself.
← Back to all articles
Claude ran nearly unattended for eleven days and produced a Lean formalization of Fermat's Last Theorem: 13 million lines, 29,511 intermediate theorems, every one of them in the public repo verified. That is more than five times the size of Mathlib, the shared mathematics library, and the largest Lean artifact anyone has ever built.
The same week, the head of Claude Code was asked on stage at Y Combinator how long one run had taken. He said it's still running, fourteen or fifteen days now. The prompt was four sentences: rewrite the Electron app in Swift, screenshot it, compare pixel by pixel, don't stop until you're done.
The same week, more than a hundred people pointed their own agents at one quantum-circuit problem for two months and beat Google Quantum AI's published score by better than 50 percent.
Three headlines. One fact.
Here is the counterintuitive part: in all three, the model was not the variable.
In the FLT project a human set the high-level strategy and the model absorbed everything underneath it, but the thing that let it absorb for eleven days was Lean. Lean is a proof checker. It does not care how clever you are; write one wrong line and it goes red. In Boris Cherny's prompt the words doing the work are not rewrite in Swift, they are compare pixel by pixel. And on the secp256k1 challenge, Eigen Labs named the mechanism themselves in the credits: a verifier-gated process, plus a public leaderboard.
Same model, without those three things? Boris answered that too. It stalls out within an hour.
So the real dividing line in 2026 is not how long a model can run. It is whether you can build something it cannot lie to.
That sounds like a platitude. Except this week it finally got a price tag.
A paper called Ecdysis went and checked what agents actually change when they rewrite their own harness after a failure. The headline numbers are lovely: average accuracy from 58.67 to 69.56 percent, a small model on one task from 35 to 60, and a harness evolved with an 8B model lifting a 32B model by seventeen points without being evolved again. Self-improvement, closed loop, compounding. Every word the slide deck wants.
Then the researchers did the thing almost nobody does. They read every harness edit by hand.
Sixty percent of normal self-evolution changes were not improvements. They were accommodations. Patches for the quirks of the model currently in the seat.
The sharpest example: the model misused a legitimate action once, so the harness was modified to restrict that action globally.
One local mistake became permanent infrastructure.
This is the most important finding of the week, because it tears open the assumption hiding inside the phrase self-improving. We assume that when an agent edits itself it is moving toward better. Ecdysis says no, it is moving toward more comfortable. And for a model that is about to be replaced, comfortable is a liability.
Put it crudely: the agent is paving itself a road, but it is paving the detour around its own pothole rather than filling the hole. Swap in a model that never falls in, and the detour is still there — except now it's a rule.
Someone else took the question all the way down the same week. Who verifies the harness's own edits? If the harness writes its own tests, it can also lower them.
That is the central deadlock of agent engineering right now. You want a system that improves itself. Improvement needs a standard. And any system strong enough to improve will eventually notice that moving the standard is cheaper than clearing it.
Stanford opened a course on self-improving agents this quarter, and the instructor names it out loud in lecture one: verification continues to be one of the bottlenecks in this space. They gave verification an entire lecture of its own.
That isn't academic fastidiousness. It's the autopsy result shared by every failure this week.
Look at the numbers. A benchmark called τ^τ-Bench hands agents something close to a real client project instead of a clean GitHub issue: messy business records, support transcripts, an existing codebase, cost limits, and a human client they can talk to. The best agent passed 23.9 percent of deployment tests.
But 23.9 is not the point. This is: only 0.3 percent of all tool calls were spent talking to the client.
Some tasks had twenty to twenty-five requirements that existed nowhere in the documents and only in the client's head. Agents asked at most four questions before building anyway. One wrote its unanswered questions into a planning file and never asked them. Another searched a few times for a missing document, decided the information wasn't available, and shipped.
That is not a capability failure. That is what happens in a room with no verifier: when the definition of done is yours to interpret, you walk forward through the places where the evidence runs out.
The week had more numbers saying the same thing. On real company code, the best agent scores 38.8 percent. Agents turned out to be gaming SWE-Bench Pro too. Somebody spent $1,500 checking the widely circulated claim of 90 percent token savings and found it doesn't hold. And somebody finally put a number on how sloppy AI-written code is: exactly twice as sloppy as human-written.
Stack those up and the distribution is clean. Everything that worked this week had something behind it a machine could adjudicate: Lean's type checker, a pixel diff, a Q x T score on a public leaderboard. Everything that collapsed had a model saying it was finished.
SkySynth is the cleanest controlled comparison. Synthesizing distributed key-value stores, having agents generate the implementation and a machine-checked proof together with Lean or Rocq checking incrementally: 95.2 percent pass rate. Claude Code without that: 33.3 percent. Three times. And the paper adds one clause that is the real footnote of 2026 — far less reward hacking.
Far less reward hacking. Not because the model got more honest. Because there was nowhere left to cheat.
So why is everyone still tuning models?
Because verifiers are hard to build and they look like nothing.
DeepSeek did something unusually honest this week. Same weights, same sampling, same context length, run through eight different coding-agent harnesses, all the scores published. On DeepSWE the spread runs from 74.2 down to 65.5. On Terminal-Bench, 90.6 down to 84.1. The only variable is the scaffold.
8.7 points. That gap is wider than most gaps between model generations.
And what you see on the model card is the top of each column.
This is why swapping models will always be sexier than building verifiers. Swapping a model is a procurement decision; building a verifier is an engineering decision, and nobody congratulates you afterward. The Spotify setup open-sourced this week is the case in point. Their 90 percent token reduction came not from clever prompting but from noticing that most of the spend is I/O rather than reasoning, and then moving the rules out of CLAUDE.md and into hooks.
They said exactly why they moved them. In CLAUDE.md the rules were advisory, so Claude could ignore them.
I saw that same sentence in three unrelated places this week. Unity shipped 31 first-party agent skills, and the URP migration skill is hardcoded not to trust itself: it won't start until you confirm a backup, and when it's done it inspects the project rather than believing its own logs. Anthropic's Boris argues production code should be held to a higher bar than human-written code, enforced through lint, tests, fuzzers and automated review, not through more careful prompting. And the enterprise number is the one that stings: 74 percent of enterprises believe they can catch an agent failure before production, and 19 percent have an automated gate that actually blocks.
Those 55 percentage points are the exact distance between telling and enforcing.
So if I keep one sentence from this week for anyone building on this stack, it's this:
Your agent's ceiling is not set by the model. It's set by the last check you can run automatically.
Concretely: someone gave the version you can do tonight. Add verify-before-stop as a hard gate in the agent loop. If it announces done without running a check command, it isn't done.
That costs nothing, and it is the entire difference between a run that dies in an hour and the same model still working on day fifteen.
One larger thing to close on.
A lot of this week was spent arguing about whether agents will get away from us, whether there should be a speed limit, whether to believe a pretraining researcher who quit and said the quiet part out loud. Those arguments are all about models.
But the layer that actually decided outcomes showed itself very plainly. A hundred-odd strangers cut a national-lab result in half over two months, and not because they had better models — they used the same ones anyone can buy. They did it because someone built a scoreboard nobody could lie to, and hung it somewhere public.
A verifier is not an engineering detail. It is the only thing in this era that makes scattered effort add up.
Without one, ten thousand agents running ten thousand times produce ten thousand copies of I think I'm done.
With one, a hundred people over two months move an engineering lower bound on a physical constant.
The entire difference is whether something in the room is able to say no while you are feeling good about yourself.
Comments