I would say that learning TLA+ is first and foremost learning how to describe systems using mathematics. It isn't at all as scary as it may sound, but it also v

I would say that learning TLA+ is first and foremost learning how to describe systems using mathematics. It isn't at all as scary as it may sound, but it also very much isn't the same as describing a system in code. You definitely don't have to learn to do that to use some formal verification tools, but that is what you commit to learning when you choose to learn TLA+ specifically. That is because the assumption behind the design of TLA+ is that using mathematics is ultimately the easiest and clearest way to describe certain important things you may wish to know about programs. TLA+ is a produce of the nineties, and the specification languages that preceded TLA+ in the eighties used more programming-like approaches. And TLA+'s novelty came largely from abandoning the programming approach. It is a later, rather than an earlier evolutionary step. However, if you accept that you won't be able to describe such things, certainly not easily, then there are other languages and tools that don't require a mathematical approach -- some predate TLA+ and some are later, but follow the earlier approach of the 1980s.