On 22 October 2026 Anthropic's Frontier Red Team published a piece with a title that gets straight to it: large language models are making formal software verification feasible at a much larger scale. Two days earlier, the same team had put out another one on using Claude to shrink the attack surface of code. Some outlets have boiled this down to "Claude writes code and proves it safe, on its own". That summary overshoots, but underneath it there is something I think is one of the more serious developments of the year.
What happened
The Frontier Red Team page now lists 34 posts and, scrolling down, the last year reads almost like a parallel report on offensive and defensive capability: December 2025, agents finding 4.6 million dollars' worth of exploitable flaws in smart contracts; January 2026, bug hunting across the Python ecosystem with property-based testing; 8 October, the opt-in scanner for open-source projects; 29 September, a warning about GLM-5.3 and the spread of advanced cyber capability shipped without meaningful safeguards.
And now these two latest posts, which point the other way: using the same capability to close holes instead of opening them. The technical detail is in their write-up — I'm linking the team index so you read it first-hand rather than taking my word for it — but the claim is the one in the title: what used to be possible in three or four projects in the world now fits in more places.
Why it matters
Formal verification means proving mathematically that a piece of code meets a specification. Not "I ran 400 tests and nothing blew up", but "no input exists that breaks this, and here's the proof". It's done in languages like Lean or Dafny, and the result is checked by a machine, not by a reviewer who's been up since six.
The idea was never the problem. The cost was. Writing the proof for a function costs far more than writing the function: you have to find the invariants, wrestle with the proof assistant, go round again. That's why formal verification lives in microkernels, compilers and little else. The rest of us write tests and hope.
That's where the model comes in, and the reason this works isn't that Claude is clever. It's that there's a deterministic checker at the end of the pipe. The model can produce a hundred attempted proofs, ninety-nine of them rubbish, and it doesn't matter: the checker rejects them without argument. No hallucination survives a judge that answers yes or no. It's the same pattern that makes models good at compiling, fixing tests or fuzzing, and bad at writing the annual report: where a cheap oracle exists, the model's brute force turns into results.
What someone would do differently from today. Not verify the whole application — that still makes no sense — but pick the three or four functions you genuinely cannot afford to have fail and give them a real specification. The parser that eats outside data. The amount calculation with its rounding. The authentication state machine. The concurrency bit nobody has touched since 2021 because it's frightening. Small pieces, very expensive when they break, impossible to cover exhaustively with tests.
What doesn't change
Now the small print, which here is rather large.
- A proof only proves what the specification says. If the spec is wrong, you have perfectly correct code doing the wrong thing. The bug doesn't vanish: it moves upstream, somewhere fewer people are looking.
- The trusted base is still there: the compiler, the proof checker itself, the hardware, and every boundary where your verified code calls code that isn't. That boundary is usually enormous.
- It covers none of what actually takes you down on a Tuesday: the dependency with a new maintainer, the open bucket, the secret in the logs, the backup nobody ever restored.
- "Automatically" is the headline, not the paper. What they say is that it's now feasible at larger scale. There's a gap between that and "solved", and we shouldn't close it on their behalf.
- And an uncomfortable one: the capability that writes proofs is the capability that writes exploits. The same team publishes both, and that isn't a contradiction — it's the actual map.
Our take
To me this is comfortably the most interesting thing to happen this year in AI applied to code. More than agents knocking out a CRUD in twenty minutes. And the reason is the one above: the oracle.
I've had the same rule for a while and this reinforces it. Where there's a cheap, deterministic checker, models perform absurdly well. Where the only judge is a human reading a diff at seven on a Friday, it's a lottery. All the useful effort of the next two years isn't in bigger models: it's in manufacturing oracles for places that don't have one. Formal verification is the extreme case, which is why it shows up so clearly.
What I think will age badly: the word "verified". I give it eighteen months before it appears on a landing page as a badge, and two years before someone sells "AI-verified" meaning the model had a look and thought it was fine. When you see it, ask three things: which specification, which checker and which version, and what falls outside the verified boundary. No answer to all three, it's marketing.
And one unglamorous piece of advice: before you wire Lean into your project, check whether something more basic is missing. In most codebases that reach me, property-based testing — generate thousands of random inputs and check a rule holds — gives you eighty per cent of the value for a fraction of the effort. Anthropic's own team has spent a year using that route to find bugs. Start there.
This is exactly what we run into when someone asks us to put AI into their development process: the right question isn't how much more code the model can write, it's what automatic net sits underneath to say that code is sound without anyone having to have an opinion. When that net doesn't exist, generating faster only piles up debt sooner.
Any questions, tell me and we'll go through it. All the best, Vicente.