TLA and much of the initial research in distributed systems (paxos!) came from Lamport who has been at microsoft for years now. if you look at the references in the document, many point to his work.