So the question becomes, why didn't anyone discover it?

Because it's difficult. Sure, it's obvious in hindsight, but it's a flaw in a small part of a very large and complex system.

What happened to all the theorem proving software that are supposed to absolutely guarantee correctness of code. I guess they are only as accurate as the assumptions input into them?

In this case the CPU does function exactly as designed. Any correctness prover would agree.

It does show the problem of all theorem provers: they are only as good as the specification.

The code conforms to the specification. It's not buggy.

The specification does not conform to the user's expectations or documentation. It's flawed.

Theorem provers can only prove that the code conforms to the specification, not to the user's expectations or documentation. They can be very helpful, but they aren't magic and can't interpret non-formal specifications.

Too good to be shared perhaps? I don't like this conspiracy theory way of thinking, but post-Snowden it's difficult to draw a line.