The idea of formal verification of code is kafkaesque. Its popularity is proportional to the inefficiency and irrationality of the economic system within which it exists.

Code is an expression of pure logic. So if there is any incorrect assumption or flaw in that logic, it can be verified by simply reading the code.

Given that premise, the usefulness of formal verification can be disproved in a single English sentence:

Formal verification does not remove the element of human error from a system; it removes it from the code and adds it to the system of proofs which verify that code... Proofs can be written with incorrect assumptions (human error) in the same way that code can be written with incorrect assumptions. As one of the people in the article acknowledges, writing good proofs is challenging; "challenging" inescapably means "prone to human error".

Formal verification proponents seem to have conveniently forgotten to apply formal verification to prove the effectiveness of formal verification.

The great irony of this article is that it attempts to rely on exhaustive proof (which is the basis of unit testing) to prove the effectiveness of formal proof - I.e. we tested formal verification with that helicopter that one time and the hackers couldn't hack it for 6 months, therefore formal proof is effective - That's a lousy unit test case and it doesn't prove formal verification.