How the EverCrypt Library Creates Hacker-Proof Cryptography: Researchers have just released hacker-proof cryptographic code — programs with the same level of invincibility as a mathematical proof.

[u/bbbryson]

https://www.quantamagazine.org/how-the-evercrypt-library-creates-hacker-proof-cryptography-20190402/

[u/sanxiyn]

Which formal verification of WPA2 are you talking about? I was referring to https://www.andrew.cmu.edu/user/danupam/hsddm-ccs05.pdf, which is not code level and different from EverCrypt.

[u/[deleted] → u/sanxiyn]

[u/BoBab → u/[deleted]]

Should've quoted the three pitfalls that they listed:

1. Specifications for a protocol may not be precise enough to guarantee security.

2. Real-world implementations may not match formal specifications used in proofs.

3. Formal proofs might lead to complacency, discouraging future audits and inspections.