https://media.ccc.de/v/32c3-7171-when_hardware_must_just_wor...
Software design and testing is hard, but what happens when each bug fix can cost months of delay and millions of dollars? In this talk we’ll take a behind-the-scenes look at the challenges in the design of a very complex, yet critical piece of hardware: the modern x86 CPU.(Good recent examples include the AMD lockup bug that Matt Dillon found, and the nasty counter-example of the Intel Quark segfault bug, which can't be worked around so easily because the Quark doesn't have killbits. "Oops.")
Only with the sort of engineering most current CPU manufacturers use.
It's possible to have formally verified hardware; it's just expensive with current tech. Tools are improving, though. I suspect the next cutting edge will be the unification of functional-language-to-hardware compilers like Clash or Lambda-CCC with fully dependent languages like Agda or Idris, where you can statically verify arbitrary properties though the type system.
It's hard to know exactly what's wrong without more internal, never-to-see-the-light-of-day Intel information, but it's possible the patch is as simple as tweaking the decoding, or disabling an optimization. It's doubtful a fix like this would require disabling an entire instruction set or hardware unit (like the TSX fix required; those are fairly rare bugs, even for Intel).
Specifically, given that it happens to be a bug that only happens with FMA3 disabled and hyperthreading enabled, it's probably some kind of hardware scheduling deadlock, and the patch could be as simple as "when the decoder sees this sequence of instructions, add some strategically placed NOPs to avoid the deadlock."