The elusive 100%-coverage formal spec that covers every intended and unintended input, the interests of every stakeholder, and every possible user behavior? In the vibecoding era? No, the page has the decency to acknowledge this doesn't exist.
In the end, they settle on finding crashes with a conventional fuzzer, fixing crashes, and then... writing a formal proof that the crash is fixed? That seems... pretty pointless? Am I missing something here?
> Proving that a fuzz test has no more crashes to find is more significant than it sounds. It’s common for fuzz tests in real-world code to test for violations of meaningful high-level properties, such as encode-decode roundtripping, idempotence, algebraic laws, differential testing, self-consistency, or equivalence to reference implementations. For example, a fuzz test for the LZO compression algorithm asserts that if you compress an input, then decompress it, the result is the same as the original. If the property does not hold, the program crashes—so proving the test never crashes is equivalent to proving the property itself.
However, you're correct that this is not formal verification in the sense of a correctness proof against a full specification validated to capture what the program is intended to do. Pretty impressive though.
What they did is tried to prove that the conventional fuzzer won't find crashes. Where they found counterexamples, they fixed the bug and tried again.
In essence, a fuzzer takes random samples out of a space of possible inputs that could crash. They proved that nothing in the space of possible inputs could crash.
This is a strictly more powerful result than a fuzzer could give you.