I readily use TLA+ or PlusCal whenever I am reasoning about a system which may (if buggy) experience deadlock, starvation, race conditions, etc. This includes most systems involving two or more communicating processes. (The exceptions are those systems, such as a simple pipeline, where communication is trivial and acyclic.)
It's perfectly suited to this domain of problems, which also happen to be those which are difficult for humans to reason about (owing to the sheer number of possible interleavings of execution between two or more processes).
And TLA+, an especially PlusCal, are simple enough that no system is really "too small" to be modeled. E.g. a PlusCal model of a simple pipelined server (say, reading stuff from the network and writing asynchronously to disk) is maybe ¼ to ½ the size of the actual implementation, with half as much again worth of invariants.
It's perfectly suited to this domain of problems, which also happen to be those which are difficult for humans to reason about (owing to the sheer number of possible interleavings of execution between two or more processes).
And TLA+, an especially PlusCal, are simple enough that no system is really "too small" to be modeled. E.g. a PlusCal model of a simple pipelined server (say, reading stuff from the network and writing asynchronously to disk) is maybe ¼ to ½ the size of the actual implementation, with half as much again worth of invariants.