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