I found "Specifying Systems" by Lamport, and the examples it gives, to be an excellent introduction and a stricter companion to https://learntla.com.

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.