- https://learntla.com/introduction/
- Pracitcal TLA+
It’s much easier to get running with than other formal methods tools like Isabelle and Coq.
Lamport's TLA+ book, and "Specifying Systems" are both available online (https://lamport.azurewebsites.net/tla/book.html). That one's worth a read too. Lamport's approach to teaching TLA+ is different, and probably more suited to the mathematically-inclined.
If you like spelunking through history, I'd also recommend checking out some of Lamport's papers on TLA. I particularly like "What Good is Temporal Logic?" which lays out his early arguments about why temporal logic is useful for solving some classes of problems. The paper is available here: https://www.microsoft.com/en-us/research/uploads/prod/2016/1...
Link to the book: https://www.apress.com/gp/book/9781484238288