Simulating Elevators in TLA+ is a fun exercise.

https://github.com/tlaplus/Examples/blob/master/specificatio...

Another interesting, and underrated one: hotel keys.