In short: it's great, learn it. Slightly longer, it may seem useless at first given that TLA+ doesn't verify code you write, but is rather better thought of as

In short: it's great, learn it. Slightly longer, it may seem useless at first given that TLA+ doesn't verify code you write, but is rather better thought of as a formal design language for designing abstract state machines. However, it is extremely useful for clarifying thoughts and serving as a concrete design artifact for other engineers to examine. Also because its apparent weakness that it doesn't verify code you write is in my opinion a strength because it means you don't incur a dependency on it if you or your team doesn't like it and wants to throw it away. You lose no more time than what you put in.