SQLite: 92 million lines of tests
Dijkstra: Tests can only prove the presence of bugs, never their absence!
Dijkstra: Tests can only prove the presence of bugs, never their absence!
But I had a funny experience recently where an agent implemented an entire feature completely wrong (exactly backwards, actually, in a way that defeated the purpose, introduced security issues etc.).
It happily supplied tests for the new functionality, and all the tests passed.
What I realized was, even formal verification wouldn't have helped here -- it would have just written a mathematical proof that the incorrect functionality was correctly implemented!
So there's a gap here, where first, the human's intention needs to be formally specified (by the human, or at least the human needs to be able and willing to verify it), and then the slopswarm can hack away at it...
Yes, that has always been the case with formal proofs. Even a mathematical proof with Lean is useless if the proven formal statement doesn’t match what the mathematician meant. And that’s why humans working with formal languages won’t be going away. Natural language is imprecise by nature, even when we have precise ideas in mind. In that case, it’s often better to specify what we mean in a formal language than in natural language.
This never changed with AI; in fact, I think it made this need more visible than it ever had been before. You can't get away with not being able to describe in detail what you want. As with working with humans, any ambiguities will be interpreted, and not always in the way you hoped.
Not by hand in the olden days but with AI to help with it, why not?
This is importantly different from formal code verification, in which the specification that needs to match the programmers' intentions is small enough to review, while the bulk of the LLM's output is proof tactics and such, which don't need human review because the verifier guarantees* that they're right.
I suppose you could just tell Fable "hey try using TLA+ to look for bugs in this code" and see whether it finds any.
* Uh, usually. https://leodemoura.github.io/blog/2026-8-1-postmortem-for-ke...
What do you know?
I think a model checker or something similar that can exhaustively cover a search space would suffice, though at that point I think the boundary between "test" and "formal verification" becomes somewhat fuzzy.
This is the gotcha: in stateful environments you'll have state-space explosion so big you'll have to come up with some compromising measure of "equivalent". You're right that that would constitute a proof by exhaustion of correctness. Unfortunately in practice it's entirely impractical.
[0]: demsky.eecs.uci.edu/publications/c11modelcheck.pdf
"Simple"/"complex" doesn't necessarily imply "small"/"large", respectively. Testing whether the Collatz conjecture holds is "simple", but its search space is (potentially) infinitely large. Testing correctness of concurrent data structures is (probably) a more "complex" problem, and yet it's still possible to perform exhaustive tests of their functionality [0].
In the end, the practicality of exhausting the 64-bit integer search space is irrelevant since it says nothing about the size of the write + checkpoint search space. I could just as easily say that it's easy to exhaust the 16-bit integer search space, but that doesn't mean exhaustively testing for this particular bug is easy.
[0]: http://demsky.eecs.uci.edu/publications/c11modelcheck.pdf
The union of a lot of necessary conditions is not a sufficient condition. But it might be good enough for software.
It's an art to come up with a great test suite that covers just enough and minimizes overlap, not only survives but also helps with refactoring.