Is there any way to do performance testing with TLA+? I always had the impression that TLA+ could help you validate the design of what you intend to build, but was less helpful if you wanted to see the performance implications of the design.