Temporal logic, which TLA+ is based on, provides a way to describe properties about behaviors, where a behavior is an infinite sequence of states. We could call these temporal properties or, more simply, properties. You can classify certain properties as safety or liveness properties, but those are just categorizations within the general space of properties you might care about. Roughly, a safety property is one that is violated by a finite behavior (a behavior prefix), and a liveness propert...
