Some context on this article. This article is targeted at proving programs that run on blockchain based virtual machines. These VM's are deterministic to thei

Some context on this article. This article is targeted at proving programs that run on blockchain based virtual machines. These VM's are deterministic to their core. This is quite different the envirnoments that than most programs run in. For example every time code on the EVM runs in production, it is being run in parallel on hundreds to hundreds of thousands of systems, and the outputs/storage writes/events all have to agree exactly after execution, or bad things things happen. The EVM is also single threaded, reasonably well defined, and with multiple different VM implementations in many different languages. So programs here are much easier to verify. In addition, program execution costs are paid per opcode executed, so program sizes range from hundreds of lines to about thirty thousand lines (with the high side of that being considered excessive and insane). It's again quite different than the average desktop software, or even embedded, program size. I have both used fuzzing tools (actually working on reviewing a fuzzing setup today) and formal verification in the past. I agree with the article that currently fuzzing provides a similar level of verification for considerably less effort. Current formal verification systems in the blockchain based virtual machine space are extremely difficult to write good specs for, and extremely easy to write broken specs that don't check what you think they do. On the other hand, good enough specs for fuzzing are fairly intuitive, even if great specs still take a lot of expertise. If I had a math heavy set of code that I wanted to wring the last possible security assurances from, I'd go for formal verification on top of fuzzing. But for most other work, I'd pick fuzzing. (Disclosure, I've been a customer of Trail of Bits, and worked with two of the three authors in the paper) (This isn't to say that form verification will never catch up! I'm thankful for the hard work from the people who have been moving it forward - it's gotten much better over the last two years. One day maybe it will be just as easy.)