What does LaTeX have to do with TLA+? Also I think "most of distributed systems such as AWS" might be an exaggeration. At least the public known examples of formal verification in AWS are scarce.

I think the implication is that Lamport is a proof nerd, not that LaTeX has a direct relationship to proof software.

AWS talk about it a fair amount, although rarely in a lot of detail.