You formally verify that your incorrect solution executes without a hitch, but you might just be formally verifying that any user can hit your API and download all your plaintext passwords.

Lots of security bugs are caused by incorrect specs from misunderstanding the problem and a formal verifier can’t fix these. Humans can’t think through every situation either (or the bugs wouldn’t exist) SMS that’s doubly true because NOBODY understands all the interactions of the system as a whole and how changes in the part they understand affect everything else.

I’m not saying formal verification is bad, but it’s not a panacea and I’d wager would only fix a small percentage of existing bugs.

I understand that formal verification is not panacea.

My issue is that the systems today can't even tell for certain "This network-connected program doesn't execute arbitrary code".

We can have a common list of our demands to software. We can eliminate entire classes of issues. We can understand what the software does.

I think this is exactly it though. Instead of targeting the moving target of "correctness", we should be proving the absence of common defects. Proving that secrets CANNOT be downloaded is a very nice example actually:

    * Understandable
    * Portable across projects, you could imagine something like
        from specs import no_stealing_secrets
        no_stealing_secrets(secret_table)
    * Implicitly proves the absence of RCE, though I suppose
        it could allow something truly crazy like an interpreter
        that will run any attacker supplied program that can 
        be proven not to steal the specified secrets