Speaking as a person who teaches both TLA+ and Alloy, I have a sneaking suspicion that the best way to learn the idea of model checking is _none of the three_.

Speaking as a person who teaches both TLA+ and Alloy, I have a sneaking suspicion that the best way to learn the idea of model checking is _none of the three_. I haven't seriously sat down and deep dived yet, but I'm really liking what I've seen of Runway: https://runway.systems/ https://runway.systems/. It's advantages over all three are 1. A repl 2. A repl 3. You can try it online 4. Oh my god, there's a repl The core hasn't been updated in three years, so I'm not as ludicrously-overhyped on applying it to real systems, but to build your model thinking? I really like what I've seen so far.