Note that existence of a formal proof for security is no silver bullet. A real world example of this is the WPA2 key exchange's formal proofs not catching the K

Note that existence of a formal proof for security is no silver bullet. A real world example of this is the WPA2 key exchange's formal proofs not catching the KRACK vulnerability. https://galois.com/blog/2017/10/formal-methods-krack-vulnerability/ https://galois.com/blog/2017/10/formal-methods-krack-vulnera... That being said, it's a very valuable tool and should be applied more, not less.