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.
formalnethods
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.
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.
formalnethodsAh 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.