A walkthrough tutorial of TLA+ and its tools: analyzing a blocking queue | Heykuki News