Amazon have used it to verify algorithms in several of the core distributed systems they run apparently. There was an article in the communications of the ACM recently about it, can't remember the reference offhand.
You two beat me to it haha. It was very exciting for me to see a company such as Amazon using a tool such as TLA+. I liked their careful, evidence-based approach to exploring and using the tool. Hopefully, a mainstream company using such tools will lead to a lot more interesting in using them.
