Practical TLA+ is indeed a great place to start, and Hillel Wayne's writing out formal methods is all worth reading. Lamport's TLA+ book, and "Specifying Syste

Practical TLA+ is indeed a great place to start, and Hillel Wayne's writing out formal methods is all worth reading. Lamport's TLA+ book, and "Specifying Systems" are both available online (https://lamport.azurewebsites.net/tla/book.html 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/12/What-Good-Is-Temporal-Logic.pdf https://www.microsoft.com/en-us/research/uploads/prod/2016/1...