That's definitely the main use. But TLA+ can also be applied to single threaded specifications by encoding various invariants (pre/post conditions on entry and exit, loop invariants).