形式化规范

我们如何在生产环境中持续验证形式化规范

Datadog 的工程师为事件数据库 Husky 写了一份 TLA+ 形式化规范，用来描述系统哪些状态是合法的。问题是，规范只写一次，系统却一直在改，几年后放置逻辑变了，允许两个冲突的放置同时存在约一年，平时没事，但一旦放置数据丢失、系统回填时，两个冲突就足以让回填崩溃。他们做了 FETCh 工具，把 TLA+ 规范变成运行时的检查器，拿真实生产行为对照规范，于是发现了常规测试没抓到的这个 bug。对读者的意义是：形式化规范可以和线上系统持续对账，避免规范悄悄过期带来的虚假安全感；目前这是 Datadog 自建并用于 Husky 路由系统的实践。