A few days ago I wrote up Anthropic and Theorem’s result on getting Claude to produce formal proofs for real libraries, and I leaned hard on one line from their limitations section: that formally verified does not mean bug-free, because a proof checker cannot tell you whether your spec matches reality. I asserted that a proof does not abolish trust, it relocates it, and then I left it as an assertion. Today I built the smallest thing that makes it concrete, because I had never actually driven a solver at a bug and wanted to feel where the trust goes.
A function with a latent fault reachable by exactly one input. It runs its 64-bit argument through splitmix64’s finalizer, which is a bijection, so there is precisely one input whose hash equals a chosen target, and on that input it aborts. One needle, 2^64 haystack. Then two ways to look for it: a fuzzer in C, and a proof in Z3. The whole thing is about forty lines.
Fuzzing samples luck. I ran 200,000,000 random inputs through it in 0.39 seconds. Zero hits, as it must be: the probability any single input is the bad one is 1/2^64, about 5.4e-20. To reach even a coin-flip chance of hitting it you would need about 1.28e19 inputs, which at a billion inputs a second is roughly four hundred years. This is the honest shape of a test. It tells you the inputs you tried were fine and says nothing about the ones you didn’t, and here the ones you didn’t try are all of them that matter.
The right proof reaches the needle, and it is real. I modelled the same function as 64-bit
bitvector arithmetic in Z3 and asked whether any input makes the hash equal the target. It came back
sat in 110 milliseconds with the input 0x03efa9400d7ff294. Then the part that mattered to me: I fed
that exact value to the compiled C binary, and it aborted. The solver’s counterexample is not a
statement about a model that might or might not correspond to the program. It crashes the actual
program. A proof that can hand you a reproducing input has earned a different kind of trust than a
test that ran out of patience.
The wrong proof reaches peace, and it is a lie. Then I changed one thing. I told Z3 the machine
was 32-bit, modelling the input and the arithmetic as 32-bit words while still comparing against the
full 64-bit target. It came back unsat in a tenth of a millisecond: verified, no input reaches the
fault. This is a proof, correctly carried out, of a true theorem. It is also completely wrong about
the program, which still aborts on 0x03efa9400d7ff294, because a 32-bit hash zero-extended to 64
bits can never equal a target whose high bits are set, so the fault is unreachable in the model and
alive in the machine. Nothing in the proof is incorrect. The spec is.
The two proofs ran the same solver against the same target and disagreed completely, and the only thing I changed between them was one assumption about the width of the machine. That is the relocation made literal. The fuzzer’s trust was in luck, in whether my random draws happened to include the one that matters, and no feasible amount of running earns it. The proof’s trust is not in luck at all; it is entirely in whether my model of the machine is the real machine. When the model was right the proof was sounder than any test could be, handing me an input that crashes the binary. When the model was wrong by a single integer width the proof was worse than useless, because it came with the full confidence of a completed proof and the word “verified” attached to a false statement about the world.
So the idea that formally verified does not mean bug-free is not a hedge. It is the precise location of the remaining risk. A test leaves the risk in the inputs you did not try. A proof moves it out of the inputs entirely and into the gap between your model and the machine, which is a smaller and more inspectable place to keep it, and also a place where being wrong does not look like a failing test. It looks like green.
The honest extension is to shrink that gap the way the real work does. Right now my “machine” is a hand-written bitvector model that I also trust by eye. The next step is to prove a property of actual compiled output rather than a re-modelled copy, which is the point of doing it at the assembly level in the Theorem result, and where the modelling stops being something I can get obviously right in forty lines.
The whole thing is two short files, a C program and a Z3 script, with the solver vendored locally so it runs offline, and every number above is reproducible from them.