Formal Verification: When Intention Is Not Enough

I’ll start today’s article off with a definition of formal verification as provided by Keagan McLelland on the Bitcoin Development Mailing List: Formal Verification is a practice in software development that gives greater assurances than typical testing procedures or forum arguments on how various schemes, protocols, and implementations behave. When we argue about how Bitcoin is designed or how it ought to be designed, engineers will make statements of fact about how the system works, but depending on how much effort is put into the presentation of that argument, it can be difficult to tell if a statement is true, or if it is, why it is true. By formally specifying these statements of fact on how the Bitcoin protocol works we can be precise about what we are saying, what properties we have, what properties we want, and whether the system actually delivers those properties or not. Normal programming languages do this to an extent, and indeed one of the best ways to settle a dispute is…