分布式系统很难只通过测试保证正确，调试系统bug令人头疼-MTV学习库

我们认为，我们不应该遵循传统的软件工程流程，先开发程序，然后测试程序。这是不高效、不科学的。相反，使用规范来验证程序。设计规范并使用规范验证程序尽可能地“左移”，即尽早暴露错误。

我们可以先编写TLA+规范，保证设计正确，然后按照规范编写程序，最后利用模型生成的状态空间对程序进行验证和测试，保证设计和实现的一致性。我们开发了规范驱动的开发工具包来协助完成上述工作。形式化方法不那么学术化，离实践还很远。、、等大大小小的工厂都在自己的系统中应用，节省了大量的开发成本。

如果把分布式系统比作每秒30帧的4K视频，那么我们的工具就相当于提取关键帧，降低清晰度和压缩，制作幻灯片。最后，目标是使幻灯片表现出预期的效果。用更专业的语言来说：The 是 the 的。