A walkthrough tutorial of TLA+ and its tools: analyzing a blocking queue (github.com)

This is the coolest demonstration of TLA+ I've seen to date. It takes you through specification, implementation, model-checking with TLC, visualization and animation, checking an inductive invariant, deductive proofs mechanically checked by TLAPS, refinement mapping and even model-based trace checking.

If anyone is trying to learn TLA+, this site looks like a good one: https://learntla.com/ too