It looks like the diagrams are actually animations, maybe with more step-by-step explanation, in the recording: https://www.youtube.com/watch?v=x9zSynTfLDE
Maybe there’s a tag related to proof assistants but I couldn’t find it.
Ah thank you.
TLA+ does support automated proofs with TLAPS, but it looks like they aren’t actually proving things here. They’re doing model checking.