Interesting. Here's the paper amazon published: http://research.microsoft.com/en-us/um/people/lamport/tla/fo...

It's only covering a few use cases and doesn't go into too much detail and shows example code but it seems like using TLA+ has been beneficial for them.