symbolic model checking is not easy to implement for an expressive language such as TLA+. For example, some form of type inference is necessary in order to know how to symbolically represent the value of a variable. The explicit construction of successor states by interpreting the next-state relation is much easier to implement. Moreover, it is not a given that symbolic model checking is always superior to explicit-state model checking. For example, asynchronous systems whose processes communicate via FIFO channels tend to give rise to state spaces for which no good symbolic representation is known.
However, a symbolic model checker for TLA+ is being built , and we hope that it will become a useful complement to TLC. You may also want to experiment with ProB that supports a subset of TLA+  and contains implementations of symbolic model checking algorithms .