Questions I wondered about that weren't answered until the end of the paper: Q: Do engineers actually implement AWS systems in TLA+? A: No, TLA+ is called "exh

Questions I wondered about that weren't answered until the end of the paper: Q: Do engineers actually implement AWS systems in TLA+? A: No, TLA+ is called "exhaustively testable pseudo-code" internally, and is only used for designs. Q: Which AWS systems use it? A: The first was DynamoDB, followed by S3, and now there are 8 additional complex systems that use it for designs. Q: Who uses TLA+ at Amazon? A: All engineers, from entry level to principal. I thought it was especially interesting that several engineers at AWS were effectively writing their own model checkers by writing programs that tried to brute force rare combinations of conditions that would lead to system failure. Obviously TLA+ does this better and faster so they switched to that.