out of curiosity, how did you get comfortable with temporal logic? i’ve had a hard time finding good resources aside from H. Wayne’s stuff on TLA+
It has some chapters that give very precise definitions of how things work in TLA (both on a language level as well as model checking), which answered some questions I often had along the way in more informal introductions.