Flow analysis and SMT solvers are mathematically-sound, so if done correctly, a fuzzer would have no luck finding a path through the code where any undefined be

Flow analysis and SMT solvers are mathematically-sound, so if done correctly, a fuzzer would have no luck finding a path through the code where any undefined behavior (or behavior that violates the contracts you've specified) could take place. Getting started with SPARK, you'll see messages like "Can't prove that this variable won't overflow" (usually with corner cases like "when x = 4,294,967,295 and y = -1"). So it kind of makes you realize how error-prone code can be. A statement like "x++" has the assumption baked into it that x isn't going to be INT_MAX. Fuzzers work by manipulating your control flow such that x _will_ be INT_MAX and cause an overflow or other bad stuff. Formal verification exposes all those assumptions and when people complain about slow development, it's because you're basically making the code "fuzzer-proof". "Hacker-proof" is hyperbole, but not as much as some might have you believe. People have pointed out that the specification has to be correct. My code in the pastebin proves every element in the output array is even, but if the code is supposed to produce an array of odd numbers, then obviously that's still a bug, even though it's been "formally verified". I wouldn't use the term "hacker-proof", but I would say "hacker-resistant". FV _can_ eliminate whole classes of vulnerabilities that attackers could otherwise use. A common trope is "well there's still hardware bugs or the spec could be wrong, so why bother?" I mean, sure, a hacker could cut the power to the datacenter, too, but IMO that's not a reason to ignore tools that can make the software we write much more robust. One issue that can crop up is that you can't always prove what you're trying to specify. The state space can grow too big and the solver can't figure it out in a timely fashion, so you have to make assumptions and hope your tests give you enough confidence to deploy the system. This is basically the halting problem - it doesn't say that it's impossible to prove termination (or any other property) of some code, it just says that you can't _always_ prove them. nVidia recently began using SPARK in some of their work, the video does a good job explaining some of the bugs that FV eliminates: https://www.youtube.com/watch?v=DZSSyWlsb28 https://www.youtube.com/watch?v=DZSSyWlsb28