[colonelcanoe]

You can construct formal proofs about a TLA+ spec, using the "TLA proof system" (TLAPS). Or, you can verify properties for "bounded models" of your spec via brute force.

The latter is much less overhead, so it's good to use bounded models (with the TLC model checker) to become confident in the spec, then construct proofs if warranted.