Does TLA+ system prove the model or does it verify the model by essentially brute-forceing it? AlLoy seem to do the brute force verification using SAT solvers.
Note that TLA+ is the language that the model is written in. The program validating is called TLC, it's a model checker.
tlc still has some advantages over apalache in some conditions, but actually I've never even used apalache with my models (I'm still in the practice phase, though).