How should I get started with TLA+? I don’t have any experience.
Lamport's Specifying Systems (2002, linked above) is a great book. It covers ground quickly but has deep roots - you can tell Lamport is an expert logician who engineered the language carefully. I recommend you read the first two chapters of that (free) book before you do anything else, but you may feel like you're wading through mud if you don't start writing simple specs and watch his or other tutorials by chapter 5. Most of his example specifications (Chapter 5, Chapter 11) design a memory interface for a computer, and they suppose you are familiar with basic computer architecture. If not, you'll have to learn TLA+ while learning how a memory interface works at the same time, which takes dedication.
The appeal to me of TLA+ is using set theory and first-order predicate logic to describe any system, from a poker game to a shopping trip to a computer program - anything at all where the next state depends on the history of the system after a set of initial states. The TLA+ Toolbox IDE has a TLA+ model checker called TLC that can test your logic, and that is particularly useful for a complex concurrent or distributed system if you ever design one.