WPA2 also had an exploit (KRACK) while the handshake algorithm itself was "proven to be secure". Formal verification is a powerful tool but it does not guarantee bug-free code: it merely guarantees that the particular bugs you checked for are not possible.

But if you need to make an update to a core system that'll necessitate updating the tests and you're back to flying blind.

You write tests for your code as it exists to make sure it functions. You cannot write tests for every conceivable change that someone else might make in the future that either mis-uses your code or adds new code inbetween that didn't previously exist. You need the people who add that new code to write new tests. Something that it seems the remaining engineers at Twitter do not have time for.