The TLA+ tool that they&#x27;re using is actually open source. You can read about it here (and there&#x27;s a link to the source on CodePlex):<p><a href="http:&#x2F;&#x2F;research.microsoft.com&#x2F;en-us&#x2F;um&#x2F;people&#x2F;lamport&#x2F;tla&#x2F;tla.html" rel="nofollow">http:&#x2F;&#x2F;research.microsoft.com&#x2F;en-us&#x2F;um&#x2F;people&#x2F;lamport&#x2F;tla&#x2F;tl...</a>