In the defence of TLA+ I was a complete newbie.
I mention it only because certain parts of the experience shared the maths-looking big-sequence-of-ands-and-ors one sometimes sees when dealing with complex type systems. TLA+, very sensibly, lets you break up complex statements into multiple smaller statements and give them names.
I was simulating the behaviour of two ends of a communication channel which had been designed with a bidirectional message number/acknowledge/timeout/resend mechanism. And both a hardware and a software state machine on each end managing the message queue in each direction.
The experience was in equal parts brilliant and frustrating. Brilliant because it did reveal faults in the design that probably couldn't have been found any other way. Frustrating because (for example) if you represent your timeout mechanism as a counter on each end of the link and which can only count from 0 to 2 the check will succeed in a few seconds. But if you change the timeout behaviour to count from 0 to 10 the check will take a lot longer. I don't know exactly how long because I aborted the run after a week. And there was no real indication of precisely why it'd stopped completing - I basically had to undo my changes one line at a time until I figured out what was going on.
TLA+ also seemed to have some sort of TeX integration. So a lot of the documentation is written in TeX - it's a fine way of writing math I'm sure. But sometimes the documentation told you how to do something and showed an example statement with a dot, yet you couldn't copy-and-paste the example from the documentation into your code, to express it in your source code you had to use something like \cdot or \circ instead.
Interesting stuff to try out for sure. And impressive given the size of the team that works on it, which I gather is tiny.