If I wrote a simple BFS or DFS and enumerated the search space how far would I get.. Is that not what TLA+ does in principle.
I am surprised people prefer having a dependency of something like Z3 at compiler level.
This is an extension of the CDCL (conflict driven clause learning) approach to SAT solving, which is a heuristic approach that uses information discovered about the structure of the problem to reduce the search space as it progresses. At a high level:
1. assign true or false to a random value
2. propagate all implications
3. if a conflict is discovered (i.e. a variable is implied to be both true and false):
1. analyze the implication graph and find the assignments that implied the conflict
2. Add a new constraint with the negation of the assignment that caused the conflict
3. backtrack until before the first assignment involved in the conflict was made
While there is a series of "standard" techniques for encoding particular program languages features into SMT (e.g., handling higher-order functions, which SMT solves don't handle natively), the details of how you encode the model/properties are extremely specific to each formalism, and you need to be very careful to ensure that the encoding is sound. You'd need to go and read the relevant papers to see how this is done.
It looks like the TLA+ Proof System does the same thing, but I believe you can also use TLA+ in "brute force all the states" mode. I haven't actually used it.
It looks like there are some TLA+ implementations that do use SMT solvers under the hood.