He later in the post shows invariants which cannot be verified as assertions within the system (e.g. as a process within a distributed application), because the

He later in the post shows invariants which cannot be verified as assertions within the system (e.g. as a process within a distributed application), because they rely on having an omniscient view of the system (e.g. access the state of all processes in the distributed system at one point in time). I think that's where the distinction makes sense. Of course you'll likely still turn those invariants into assertions, but in some kind of simulator which can view the complete state of the system rather than in the system itself.