I read through a chunk of Lamport’s book and the first 7 or so sections of his online course (the rest weren’t posted yet).

https://lamport.azurewebsites.net/tla/tla.html

https://learntla.com/introduction/

Is also a good introduction. That was enough to make me dangerous. Since work didn’t have an interest in training me, and I had other obligations, that’s all I’ve done so far.