Yeah. And TLA+ can confirm that the design is sound, but it can’t confirm that the implementation conforms to the design. QuickCheck style tests can’t solve that problem, but perhaps they can mitigate it.