As others have said, TLA+ can be very useful outside distributed systems. For example, I'm currently working on a virtualization-related low-level systems paper

As others have said, TLA+ can be very useful outside distributed systems. For example, I'm currently working on a virtualization-related low-level systems paper (likely to be submitted to VEE) where we use TLA+ to reason about the safety of some new syscalls and their related programming patterns. Reordering and concurrency of interactions between processes and the kernel can lead to many of the same challenges as distributed systems. Many people have also used TLA+ for business logic reasoning, but I haven't yet tried it in that domain (I tend to just do state machine stuff, and sometimes use Alloy).