Put simply, formal verification uses math to specify and analyze a program for errors in logic. However, because of the time and cost involved, formal verification is best reserved for situations where human life or large sums of money are at stake.
Currently, formal verification is used to verify the correctness of high-risk code in transportation, the military and cryptography. Chip companies use it to fortify algorithms before embedding them in silicon. And banks use it to develop financial algorithms.
Applied to blockchain technology, formal verification could provide assurances that self-executing transactions known as smart contracts will work as intended, eliminating some of the bugs and financial losses that come as a result of coding errors.
This year alone, bugs in Ethereum’s Parity wallet accounted for $180 million in losses. Last year, a bug in a virtual organization known as The DAO enabled a hacker to siphon $50 million from the Ethereum smart contract.
Platforms like Cardano and Tezos are already working on smart contract languages specifically designed to facilitate formal verification. Ethereum is also working on bringing formal verification to its smart contracts.
But what is formal verification? How does it work? And why is software so difficult to get right in the first place?
To Err Is Human
Software is inherently unforgiving. If you are constructing a building, you can leave out a nail or a screw, and the structure still stands. But when it comes to software, something as simple as a single typo can cause the entire program to stop working.
“Programming languages are incredibly powerful,” Gerard Holzmann, former lead scientist at NASA, explained in an interview with Bitcoin Magazine. “As a programmer, you have to deal with a lot of detail, and unless you get every detail right, there is some effect.” […]