1. 13
  1.  

  2. 3

    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

    1. 1

      Maybe there’s a tag related to proof assistants but I couldn’t find it.

      1. 2

        formalnethods

        1. 1

          Ah thank you.

        2. 1

          TLA+ does support automated proofs with TLAPS, but it looks like they aren’t actually proving things here. They’re doing model checking.