Leslie Lamport built latex, most of distributed systems such as AWS services depend on formal verification. The job of Science here is to help Engineering with managing complexity and scale. The researchers are doing their jobs
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.