Interesting that they used both Lean and TLA+. I wish they'd speak more about that. I woulda thought they'd use one or the other. Generally speaking they both do the same thing (prove specs), but in very different ways.