TLA+ lets you work at much different scales. I have one spec I'm working on where the "___domain model" is multiple nodes trying to reach consensus, where some fraction of the nodes are adversarial and intentionally trying to subvert the others. With that you can ask questions like "what is the maximum fraction that can be adversarial and still guarantee these specific global system properties."

Another one involved modeling several microservices, each of which had its own team and codebase. That kind of scale is really hard to do at the lines-of-code level of verification.