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...