Improving System Safety with Temporal Logic of Actions

Depot 团队让 agent 把 Go、SQL 和 S3 组成的实现翻译成 TLA+ 模型，再由工程师审查抽象与不变量；模型检查了 14,290,224 个不同状态，耗时约 21 分钟，覆盖 10 条安全属性和 2 条活性属性。检查发现一个垃圾回收竞态：相同摘要在 MySQL 引用检查与 S3 删除之间被重新推送时，仍在使用的 blob 可能被删。修复使用 S3 version ID 作为删除栅栏，只删除检查过的确切版本；案例也表明 agent 能加速形式化建模，但状态抽象和性质选择仍是人的核心责任。