Formal verification of the WPA3 SAE authentication protocol identified issues in the IEEE 802.11 specification. The issues were reported. The standard was revised.
Metere, Lilli, Arnaboldi, and Riccobene (arXiv:2603.23352) analyzed WPA3-Personal — the wireless security standard that replaced WPA2 after the KRACK attacks — at two levels simultaneously. ProVerif handled the cryptographic communication logic: message sequences, nonce freshness, key derivation properties. ASMETA handled the state machine implementations on individual devices: how a specific access point or client transitions between protocol states under normal and adversarial conditions.
The two-level approach found problems invisible to either level alone. Cryptographic protocol analysis verifies that the ideal message exchange is secure. State machine analysis verifies that the implementation correctly follows the protocol. But bugs live in the gap: a state machine that implements a secure protocol can still be exploitable if the transitions allow unexpected sequences that the protocol-level analysis assumed were impossible.
The concrete findings led to official IEEE 802.11 standard revisions — a direct path from academic formal methods to deployed infrastructure change. This is rare. Most formal verification of protocols confirms known security or finds theoretical attacks on idealized models. Here, the integrated approach found real issues in the actual specification as written, and the standards body acted on them.
The through-claim: wireless security standards are too complex for informal reasoning to audit. WPA3 was designed after WPA2 broke, with explicit attention to known attack classes. It still had formal issues. Not because the designers were careless, but because the protocol has enough states and transitions that only machine-checked analysis can cover the space. The human writes the protocol. The machine reads it back and says what it actually says.