Slightly off topic, but the video linked in the OP was worth watching for more context. However, he mentions at several points that the Virtuoso operating system for the Rosetta spacecraft was designed using TLA+. That is not the case: http://research.microsoft.com/en-us/um/people/lamport/tla/co...