From TFA "And separately, to answer a question: how did this attack slip through, despite the fact that the 802.11i handshake was formally proven secure?" Imp

From TFA "And separately, to answer a question: how did this attack slip through, despite the fact that the 802.11i handshake was formally proven secure?" Implies that the formal verification failed. Yet from the paper on the attack: "Interestingly, our attacks do not violate the security properties proven in formal analysis of the 4-way and group key handshake." This is a good thing! One of the hard things for software developers to do is separate the theorem (spec) from the proof (implementation). I can see how the article author would posit such a question. The paper answers the question. What do we do about it? More theorems, modelling, and proofs. Research on synthesizing the implementation from its specification. Treat events like this as we treat auto-collisions and correct the processes, tools, and technology that enable attacks like this to occur in our systems... at least that's my 0.02. :)