SAT and SMT solvers deal with propositional logic only. TLA+ is based on propositional logic with added modalities (i.e. what a type theorist would call monads) for "time" (in the temporal logic sense) and non-determinism. It is essentially a somewhat bespoke modal logic. Modal logics in general have lower expressive power than FOL, but are conversely more computationally tractable.
Sounds like the first thing TLAPS does is to translate the TLA+ program into SMT and try to prove it with Z3. If that times out then it translates it into a couple of other kinds of provers before giving up (...).
Maybe I should look at how TLA+ "hello world" is compiled into SMT as a first step.
