1. 13
    1. 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

    2. 1

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

      1. 2


        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.