Posted by johnbender 11 hours ago
Is formal verification the path forward? Meh... I dont think so. Does it have applications in some areas: yes. But this is just more robust "unit testing".
Anthropic keeps trying to convince you that "one agent" will do the job. It does so with the statement "We built 36 small verification tasks from real OSS-Fuzz code. Opus 5.5 proves half of them with about 40% fewer tokens than Opus 5. We expect this trend to continue as models are trained on long verification tasks."
But this is not the path forward. Robust E2E, durable (can your app go from python to rust with out loosing tests) Simulation/Emulation tests are the way. This is an "in bulk" and "brute force" activity. Go look at TigerBeetle for an example of this in practice. Go look at how oxide is doing testing.
Can a swarm of cheaper agents write these tests more effectively that Anthropics premium products. I assure you that it can.
If you look at OAI's actions (hugging face hack) and anthropic own publication on its version control AI is not a best of breed solution its a brute force hammer at it till you get what you need solution.
I wish people would learn a little computer science before making this kind of impossible claim. And I wonder how many people read claims like this and accept them without investigation.
The Turing Halting Problem (THP) invalidates the above claim, on all nontrivial software systems, forever.
The THP (1937) is derived from Gödel's Incompleteness Theorems (1931), and the latter are not a matter of opinion.
For those with limited attention spans, ask yourself this: How does the foolproof program checker check itself?
Pop-sci explanations of the halting problem have probably done incredible damage to formal verification as a whole. Mostly because it makes people with only the most cursory understanding of it go "why bother, it won't work anyway."
But most real-world programs are maybe not that "expressive" since we don't even want them to be capable of infinite loops (since those would often be denial of service vectors). So you should usually be able to prove that they halt (and presumably other properties as well), especially when you allow agents to rewrite things to pull out invariants that make proofs easier (as they did).
And for cases where getting clean invariants are difficult, I imagine you can just hack it by having some cutoff which trivially ensures things always halt. (Not sure what the equivalent would be for "no bug" proofs, probably rejecting things that are technically valid input per spec but seem unusual?)
I would say, in practice, you are more likely to encounter complexity barrier (we don't know how to decide some NP-hard problem fast enough) to proving things about your program than you're to encounter a true undecidability barrier (Rice theorem).
Although the prover might be smart enough to say, "this function is getting kinda complicated, let me model it as a random variable and see if it's enough". I think LLMs can kinda do it but not sure if your typical theorem provers can (it's on the level of being able to employ probabilistic proof techniques).
No, they aren't -- they are all Turing-complete, look it up. The THP applies to all non-trivial programs, meaning programs that support Peano arithmetic or anything more involved. That limitation certainly applies to all the programs you're describing.
> Pop-sci explanations of the halting problem have probably done incredible damage to formal verification as a whole.
That's pretty funny. It's not every day I hear Alan Turing and Kurt Gödel described as purveyors of "pop-sci".
> Mostly because it makes people with only the most cursory understanding of it go "why bother, it won't work anyway."
I won't try to list all the logical fallacies in your argument. You could do that if you were so inclined.