TLA+ is a formal specification language to describe design of distributed systems and then let the computer find issues with that design. The name stands for “Temporal Logic of Actions”. “Logic” means that you mostly work with boolean values and operations (you also have sequences, numbers, sets, and functions, though). “Temporal” means you can describe how your system changes over time (something will eventually happen or something always happens). And finally “Actions” means that your system is described as a state machine of states and transitions between them.
It is designed by Leslie Lamport (he’s not the one who made the IDE and verifier, though), the creator of LaTeX. Hence the syntax of TLA+ is basically LaTeX. It’s designed for mathematicians rather than programmers, and so describing imperative operation in it is mind-bending. So, Lamport later also created PlusCal, an imperative DSL that generates TLA+ code. TBH, it’s all a big mess and far cry from modern programming languages, their syntax, and conveniences, but it gets the job done.
The best place to learn TLA+ and PlusCal is learntla.com by Hillel Wayne, his blog, and his Practical TLA+ book. His materials have the benefit of being designed for engineers, rather than any math-heavy and obscure-symbols-loaded materials from Lamport. BTW, the book is dirt cheap, it almost feels like Hillel pays half of the production price for you. He himself says that he made https://learntla.com because he didn’t like that his book costs money.
Don’t worry about any materials being ever outdated, TLA+ doesn’t get any updates for 9 years.