[throwaway832975]

I don't know of any case in industry where TLA+ has been used to prove a spec correct. AFAIK it's only been used for model checking. Read the "Formal Methods at AWS" paper for details.