1/ Agent-driven formal verification isn't a panacea. But it's damn...
Doug Colkitt@0xdoug
15 views
Oct 23, 2026
~2 min read
Advertisement
1
1/ Agent-driven formal verification isn't a panacea. But it's damn close. And now we have the empirical data to back it up.
Using blinded agents, we compared formal verification against traditional code review. The results may shock you.
Using blinded agents, we compared formal verification against traditional code review. The results may shock you.
2
2/ We started by taking a representative sample of major recent exploits and vulns found in the wild. We looked at a mixture of crypto and OSS. All of the bugs were discovered after Opus 5.5's knowledge cutoff.
3
3/ The procedure for each repo was simple. We used a blinded agent with no access to the Internet, and gave it the pre-patched repo. For each repo, we asked it to do:
A) a traditional code review; and
B) write a comprehensive set of Lean theorems for full formal verification
A) a traditional code review; and
B) write a comprehensive set of Lean theorems for full formal verification
4
4/ After, an independent grader agent studied the details of the revealed security incident. (Some repos had multiple exploits, so each was graded.)
The grader assessed if the exploit was either flagged by the code review, or would have been prevented by the Lean theorems.
The grader assessed if the exploit was either flagged by the code review, or would have been prevented by the Lean theorems.
5
5/ The difference between the two respective methods was stark. Code review would have caught half of the crypto exploits, and a paltry 1/8 of the OSS exploits.
By contrast formal verification likely would have caught all of the crypto exploits, and 6/8 of the OSS exploits.
By contrast formal verification likely would have caught all of the crypto exploits, and 6/8 of the OSS exploits.
6
6/ There's been this persistent notion that formal verification isn't worth doing because "a spec can just as easily have a bug as code".
We decided to test that with real empirical evidence. And the answer is an emphatic *NO*. Especially in an age of agentic coding
We decided to test that with real empirical evidence. And the answer is an emphatic *NO*. Especially in an age of agentic coding
7
7/ Why? The cool part about working with agents, is that we were able to interview the review agents afterwards in light of their results. Like a post-game interview.
What they told us is most revealing of all. It honestly changed the way I understood agentic coding...
What they told us is most revealing of all. It honestly changed the way I understood agentic coding...
8
8/ "Justification mode: P-0566 was about the cast, so it went into explain why this is safe. Asking 'this looks dangerous; why is it OK?' is a weak question… 'find a value that breaks it' is a much better one."
9
9/ "I absorb the author's frame along with the author's code. The theorem doesn't absorb anything."
"When I read code, the code is the only model in view and every line seems to justify itself."
"When I read code, the code is the only model in view and every line seems to justify itself."
10
10/ "The theorem covers the parked-write state; my mental simulation started from the common path, with init_off = 0."
""I spent most of my attention on the mechanism that looked clever and unusual. I treated the mundane shared offset as background."
""I spent most of my attention on the mechanism that looked clever and unusual. I treated the mundane shared offset as background."
11
11/ "Writing a theorem has a fixed shape… filling in the right side made me name something outside the code. Bug-hunting has no such shape… if nothing turns up, nothing gets written down."
12
12/ At this point, if the evidence at this point doesn't convince you that formal verification is a fundamentally more secure way to do agentic coding, I'm not sure what else will.
