> Complex behavior between interconnected systems, out of the purview of the formal language (OS + database + network + developer + VM + browser + user + web server)

Isn't this what TLA+ was meant to deal with?

Not really, some components like components have a lot of properties that’s very difficult to modelize. Take latency in network, or storage performance in OS.