See section 6.4 of https://papers.mathyvanhoef.com/ccs2017.pdf https://papers.mathyvanhoef.com/ccs2017.pdf Essentially the spec was formally verified, but it t

See section 6.4 of https://papers.mathyvanhoef.com/ccs2017.pdf https://papers.mathyvanhoef.com/ccs2017.pdf Essentially the spec was formally verified, but it turned out that the formal definition of "secure" they used wasn't sufficient. Formal verification only works if you properly define all the security relavent properties that need to be proven, and the process of defining them can have errors itself.