[limmeau]

You can watch Leslie Lamport himself explaining it at https://lamport.azurewebsites.net/video/videos.html . It doesn't cover Pluscal, but goes deep into TLA+.

(BTW count the different shirts).