我们一直在思考如何进行确定性调试，并对此非常感兴趣。TLA+是一个非常宝贵的工具，可以帮助我们构建复杂的多线程和高性能系统的设计。在开始编写实际代码之前，我更喜欢先在TLA+中构建一个设计。但是TLA+只能帮助我们思考设计，并解决其中的设计缺陷。我们还需要考虑实际执行系统的问题。
我们可以有一个经过TLA+验证的设计，但是如果我们编写的代码容易受到并发性bug的攻击，而这些bug只是以一定的概率发生，那么我们该
