Yes it is essentially brute-forcing it.

Note that TLA+ is the language that the model is written in. The program validating is called TLC, it's a model checker.