The following paper was presented at ABZ'2014 last week, and is now available in the conference proceedings:
C., Why Amazon Chose TLA+, in
Abstract State Machines, Alloy, B, TLA, VDM, and Z Lecture Notes in
Computer Science Volume 8477, 2014, pp 25-39;
I'm happy to provide copies privately on request.