> I recently reviewed a paper that kept saying things like “we rigorously prove” and “we formally verify” — despite the fact that the paper contained nothing bu

> I recently reviewed a paper that kept saying things like “we rigorously prove” and “we formally verify” — despite the fact that the paper contained nothing but proof sketches Yep. Some people think "formal" means "mathematical," whereas it actually means "mechanical". A formal proof is one that can be correctly checked by a computer. > The second problem is deeper: it is extremely difficult to argue convincingly that a verification result is correct. By “correct” I mean not only “mathematically sound” but also “the result is faithful to the intent of the verification effort.” Worse. Even if we're convinced that the properties we verify are the right ones for correctness, we can only prove (even formally so) that an abstract algorithm satisfies them. We cannot prove that a system — which ultimately comprises a lot of hardware — does. On the other hand, because reducing the probability of (catastrophic) failure is all we can hope for anyway, formal verification in various forms can help do that better — i.e., reduce the probability further, and with lower cost — than traditional testing methods alone. For example, because a formal specification can be quite short, it might be easier to convince ourselves that the properties we're checking are indeed the ones we're interested in than thousands of tests. I absolutely agree, though, that formal methods researchers often make the mistake on focusing on the wrong thing when communicating the value of their work. Formal methods can never prove a system correct, but they can help make it more correct and with less effort than using traditional assurance methods alone. In other words, formal methods help catch some dangerous bugs more easily than traditional testing, and that is where their value is. Using the word "proof" when describing the goals of formal methods is doing them a disservice.