Signal 形式化验证达 80%，MIT 教授称 Wired 报道夸大其词

tegmark · x · 2026-11-12

MIT 教授 Max Tegmark 发起的开源社区项目 SignalShot（与 Lean 定理证明器团队合作，由 Beneficial AI Foundation 主导）已完成对 Signal Messenger 约 80% 的形式化安全验证，Google DeepMind 做出了规模相当、且与其互补的贡献。他批评 Wired 存在「formal-washing」——宣称验证已全部完成，实际上还有 20% 待完成，呼吁社区帮忙冲刺 100%。配图为两大里程碑（密钥协商与安全消息传递）的详细验证进度图，标注了 BAIF 与 GDM 各自完成与进行中的部分。