Two things stand out to me;
1. That the SSH protocol lacked a robust transcript hash all along, this seems like a staggering decision, and even though I'd read the RFCs, I'd never put this together. Turns out it's to allow for injection of messages designed to defeat traffic analysis? Not the right way to do it.
2. The SSH handshake had been formally verified ... and the proofs are still "true". But the researchers found non-obvious gaps between the environmental assumptions for the proofs and what is actually true in the real world. Formal verification is still the most comprehensive and exhaustive form of testing that we have, but gaps can really bite you. It is like relying Pythagoras' theorem for a triangle, but then it turns out that your triangles are on the surface of a sphere, which isn't a plane. The math itself is right, but the environment was different all along.