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.