I'm not sure what specific temporal properties you're interested in, but safety properties proven through the standard proof techniques (like inductive invariants), and at least common statements about liveness are supported.
> Liveness is about infinite number of states, but any real model checking is bounded by definition.
First, model checking is not bounded to a finite number of states in principle, and certainly not by definition[1]. Even in practice, modern, state-of-the-art model checkers do support infinite state spaces[2] -- of course, not in general, but in some cases. However, TLC, the model checker packaged with the TLA+ tools, is indeed not such a model checker, and can only check finite state spaces; it is what's known as an explicit state model checker. Second, liveness is not about an infinite number of states, but infinite behaviors, i.e. infinite sequences of states; the two are not the same.
> but to prove liveness you are almost doomed to use temporal logic.
Oh, absolutely, and after all, the TL in TLA stand for temporal logic, but the point is that proving complex liveness properties in real-world software systems is rare, simple liveness seems to be supported by TLAPS (although most people just use the model checkers), and complex temporal reasoning hardly ever comes up. That's why supporting complex temporal reasoning -- if it is indeed missing in TLAPS -- is not a priority. The features of TLA+ are in general very much driven by the needs of engineers working on real systems.
However, if you happened to come across a liveness property you wanted to but couldn't prove with TLAPS, I'd love to hear about it.
[1]: The name model checking comes from the model checking problem in logic, namely checking that a structure M (a program in the case of software) satisfies a logical proposition 𝜑, i.e., that M ⊨ 𝜑, or that M is a model of 𝜑. The name "model" comes from a logical model, i.e., a structure that satisfies a theory or a proposition.
[2]: E.g., https://cpachecker.sosy-lab.org/