Formal Verification and Bitcoin

The science of formal verification and how it matters for Bitcoin.

Formal verification is one of the more theoretical areas of computer science. It relies on the tools of mathematical logic to verify whether statements are correct. This field historically has been obscure, but recent advances in AI may bring it front and center.

I spoke with Clark Barrett, a professor of computer science at Stanford, who tells of a software bug that once led to the explosion of a rocket. The software ran an instance that forced it to convert a floating-point number into an integer. This caused the program to crash and the rocket to explode. A formal verification of the code would have avoided that problem.

Compiling is the weakest form of verification. A stronger form would be to run a battery of test cases. To see this more clearly, consider a function that divides two numbers. Without doing any internal checks, that function could run on any numerical inputs. If your test cases excluded 0, your function would still compile. But the edge case of a 0 in the denominator would cause the program to crash. Only a formal verification would catch this because it's not sufficient just to evaluate the functions on the different inputs, but rather to assess the function on its underlying logic.