Surprisingly (or unsurprisingly, depending on how much of Lamport's writing you've read) the answer is yes! Reachability properties seem like more of a branching-time logic thing but they're viable in TLA+ with some fairness assumption trickery.
It could be possible to modify TLC to more easily express & check reachability properties. This could be useful for modeling eventually-consistent systems, where the property we care about is that different replicas must be able to converge to identical views of the system, not that they necessarily do converge.
Andrew Helwer