Datadog 如何用 FETCh 在生产环境持续校验 TLA+ 形式化规范

Datadog 构建 FETCh（Formal Execution Trace Checker），将 TLA+ 形式化规范转为运行时监控器，持续用生产行为校验形式化模型。该系统已用于验证事件数据库 Husky 的路由系统，并发现一个常规测试未暴露的隐蔽缺陷：放置逻辑变更曾让冲突放置在生产中存续约一年，两个冲突放置即可导致回填系统在恢复放置数据丢失时崩溃。