I've heard Intel does use TLA+ extensively for specifying their designs and verifying their specs. But TLA+ specs are extremely high-level, so they don't capture implementation details that can lead to bugs. And model checking isn't a formal proof, only (tractably small) finite state spaces can be checked with TLC. And even there, you're only checking the invariants you specified.
That said, I'm sure there's some verification framework like SPARK for VHDL, and this feels like exactly the kind of thing it should catch.
Formal methods have been used in CPU design for nearly 40 years [1] but not yet for everything, and the methods tend to not have "round-trip-engineering" properties (e.g. TLA+ is not actually proving validity of the code you will run in production, just your description of its behavior and your idea of exhaustive test cases).
