Presumably of isolation features. I'm sure everyone knew what side channel attacks were and knew that formal verification could've helped find bugs in isolation

Presumably of isolation features. I'm sure everyone knew what side channel attacks were and knew that formal verification could've helped find bugs in isolation. They just chose not to do it, because it's only important for high-assurance, not for your regular insecure linux/bsd/windows. And I'm sure they are not going to bother with verification even after everything.