John Regehr's piano test is a thought experiment from 2011 that has aged well because it isn't about any particular tool.
You're visiting the Utah computer science department. Regehr tells you his group has proved that a particular version of OpenSSH is memory safe — no array bounds violations, no null dereferences. You believe him. Then you notice a large piano hanging from the ceiling above your chair, its rope passing through a box connected to his desktop. The box contains a remotely triggered knife. The trigger is wired to OpenSSH's SIGSEGV handler. He is about to fuzz OpenSSH with a tool that generates evil inputs.
Do you keep sitting?
Almost nobody would. That's the point. The verification result is true — suppose it is — and the conclusion you're asked to draw from it, that the handler will never fire, doesn't follow with the confidence the word "verified" implies.
Two problems, one word
Regehr names them.
The first is semantic. "Verified" is used loosely. He mentions reviewing a paper that said "we rigorously prove" and "we formally verify" while containing only proof sketches. The word carries a guarantee that the artifact often doesn't.
The second is deeper: even a correct proof shows that the implementation matches the specification. It does not show that the specification matches what you meant. A verified OpenSSH is verified against a model of OpenSSH, and the model was written by people who can be wrong about what the code is supposed to do.
There's a third problem the commenters add, and it's the one that makes the piano feel heavy: what exactly is in the trusted base? The code, or the compiler that produced it, the libraries it links, the OS scheduler, the bootloader, the CPU, the firmware in the network card and the drive? Alastair Reid's comment lists them, and the list is the argument. A proof about a C program is a proof about a C program, not about the machine that runs it.
What the test actually measures
The piano test is often read as skepticism about formal verification. I think that's the wrong reading. It's a test of the inference from "proved" to "safe to bet your life on," and it fails because the inference requires assumptions that no proof can supply:
- that the specification captures intent,
- that the trusted computing base is what you think it is,
- that the environment behaves as modeled,
- and that the proof's statement is the one you believe was proved.
Each of those is a place where a real system can be wrong while the theorem is right.
What earns trust instead
Regehr's alternative is the NASA adage: test what you fly, fly what you test. Systems become reliable by being exercised in realistic environments, by having failures studied carefully, and by feeding the results into the next iteration. That's not a rejection of proof; it's an account of where confidence actually comes from.
One commenter, Pascal Cuoq, sharpens it usefully: there's development testing, which is supposed to find flaws and improve the design, and there's verification testing, a second, independent, adversarial check where you are not supposed to find anything. A certified system is one where you've convinced the certification authority — a social process, not a mathematical one.
Another commenter, Madan Musuvathi, draws the line I'd draw: proving an algorithm sound is mathematics under assumptions; trusting an implementation is engineering. Both have merit, and conflating them is what produces the piano.
The part I'd keep
The most useful sentence is that verification "merely demonstrates that the implementation enjoys all the same bugs as the spec." That's not a disparagement. Removing the entire class of implementation-vs-spec bugs is a real achievement, especially in C, where those bugs are memory corruption.
But the class that remains — spec-vs-intent — is often the one that matters in security. A parser can be memory safe and still accept input it shouldn't. An access control check can be proved correct and still check the wrong thing.
So the piano test is a calibration device. It asks: given this proof, what would you bet? If the answer is "a lot, but not my life," you've located the boundary of what the proof covers.
Regehr's own verdict is that not many verification researchers would sit under the piano. That's not cynicism from the outside; it's the people who know best telling you what the certificate is worth. The honest response is to use the proof for what it does — eliminate a class of bugs — and to build trust in everything else the old way, by testing, by failure, and by iteration.
Source: The Piano Test for Program Verification — John Regehr.