xdcbt bug?
http://channel9.msdn.com/Events/Build/2014/3-642#time=21m46s
> A little closer to home, Lamport shared an anecdote of how his programming language even helped Microsoft avert a near-certain disaster. While writing a TLA+ specification for an IBM-developed memory system chip in the Xbox 360, a Microsoft intern discovered a bug that would cripple the game console. The IBM engineers’ first reactions were of disbelief, saying it could not possibly happen, Lamport said. However, they changed their tune a few weeks later. “Their tests would not have discovered it, and had this intern not discovered this bug, it would have gone into production; every Xbox would have crashed after four hours of use. [That’s] a nice success story.”
Source: https://www.asianscientist.com/2016/01/features/gyss-2016-le...
Famously, a Microsoft intern modeled the XBox's cache coherence protocol and caught a bug there before they went to prod.
Certainly bit flips can happen, but you can still prove that circuits obey your invariants!
(Note: TLA+ doesn't always fully prove correctness. Z3 is a more sophisticated approach but harder to apply to temporal logic)