If you interested in formal model checking using TLA+, this may of interest you. In this github repository https://github.com/gshanemiller/tla-examples find,

- tla.pdf - numerous examples

The PDF describes model checking in TLA working through minimal background (fairness, model state etc.), application in TLA, two non-trivial models, and two appendices with reference background on TLA, and its procedural cousin PlusCal.