You're partly right, formal methods don't catch problems that you assume does not happen in your assumptions (herein, the "operational semantics").

If this plan to formally verify internet algorithms included the Wi-Fi standard and implementations, the KRACK vulnerability wouldn't be an issue because it wouldn't verify (with respect to certain specifications, if they realized that those specifications were important to begin with).

But in the first place, most operational semantics on this level still stay at layers of abstraction high enough that they don't guard against Spectre and Meltdown.

Nevertheless, note that formal verification is also widely used at the microchip level.