TLA+ is the gold standard for specifying distributed systems, but the syntax is a bear. This isn't a problem anymore, AI can write specs for you! But you still need to understand temporal logic. Here's a 20-minute intro to TLA+ for the LLM era: emptysqua.re/blog/intro-t...
emptysqua.re
You can go far without writing TLA+ syntax now, but you still need to understand temporal logic.