Think of a process by which you start with a vague sketch of a system and end up with a concrete implementation in, say, C++. The latter is the highest level and least detailed. The latter is as detailed as the specification of your system will get. A prose design document of your model might sit somewhere on this spectrum very close to the vague sketch. A TLA+ spec sits somewhere in the middle. It's a refinement of the design doc with more details specified concretely, but not all of them (that's the actual implementation). But this mid-level specification is usually enough to make highly non-trivial assertions that invariants hold (safety properties) and also liveness properties are satisfied too. But keep in mind that the specification of your system is distinct from the model checking of that spec. The latter is like a test, albeit of your system not just some "unit" within your system.