FWIW: https://github.com/lemmy/lets-prove-blocking-queue/ is the sequel to Let’s Prove Leftpad with a focus on concurrency.
Video has been made public.
https://lamport.azurewebsites.net/tla/practical-tla.html?back-link=learning.html is what Lamport has to say about “Practical TLA+”.
Thanks, this inspired me to start learning TLA+ (in addition to my previous PlusCal experience) from Lamport’s video series!
(It includes PDF script/slides.)