A very useful article for the non-noob learner of TLA+! > This is the launching point into refinement, or using an entire specification as the checked property

A very useful article for the non-noob learner of TLA+! > This is the launching point into refinement, or using an entire specification as the checked property of another spec. We use the term "refinement" for those more special cases where `A` and `B` are both canonical formulas (`Init ∧ □[Next]_vars ∧ Fairness`), or, at least, both contain an initial state predicate and at least one box-action clause, but when learning, it's important to understand that there is nothing special about refinement in TLA+ from a mathematical point-of-view. Every formula in TLA+ describes a class of behaviours. The key general point to learn is that TLA+ does not distinguish between specifications and properties; they're just classes of behaviours that we can call a "system property" or a "system specification" based on how we psychologically think of it. The TLA+ formula `A ⇒ B` means that `A`'s behaviours are contained in `B`'s, and can be read as "specification A implements specification B" or "specification A satisfies property B" or "property B is an abstraction of property A" or "specification B is a generalisation of property A." All of these are just words used to describe the abstraction/refinement relation that's the very core of TLA+. So this is refinement, and `□[A]_vars` is an entire TLA+ specification, as is `□P` (it is true that TLC cannot check the specification `□(x ∈ 1..3)` but it can check the equivalent formula `x ∈ 1..3 ∧ □[x' ∈ 1..3]_x` but that doesn't make the simpler formulation any less of a valid and complete TLA+ specification of a system).