You can easily convince me that formal methods are more efficient for complex distributed systems problems, or for cryptographic protocols, or things like that. But even in systems whose whole premise is algorithmic, the hairy stuff provers are designed against are a small part of the overall coding task.

And for the kind of security this article is talking about, it's not enough to have a proven core algorithm or protocol; your dumb input parsers and output renderers and all that other boring integration code also needs to be bug-free, because those kinds of joinery are where we tend to find vulnerabilities.