I've been thinking about formal verification a lot, recently. I've dabbled in it before, but it was clear that it was only used by a small research community, and the effort required to verify anything larger than toy code would be immense. I agree with the author that there is enormous potential to use AI to automate the annoying parts of the verification process. What's more, the current security environment, in which the tiniest security flaw can quickly be exploited, suggests that provably secure code might be the future.

Others are correct to point out that formal verification is too difficult to apply to many types of application code. But there are domains where it is applicable today, and the main reason it is not used there is that developers lack the time and know-how. For example, many file format parsers are exploitable, but they are simple enough that they could be formally verified.