AI 前沿 · 每日整理
AlphaProof Code：AI 四周完成 Signal 加密代码的形式化验证
DeepMind 发布 AlphaProof Code：多智能体框架用 Lean 语言对 Signal 协议实际运行的加密代码做形式化验证，4 周完成，生成了 600 万行 Lean 代码，按以往做法需要专家团队数年；验证产物已开源，团队还把两个真实存在过的漏洞重新植入代码，系统都判定其不安全。
原文摘录
our verification process took just four weeks – a task that historically takes expert teams years（大意：我们的验证只用了四周——这项工作过去要专家团队花数年时间。）
值得肯定
验证的是 Signal 真正在跑的加密代码，不是玩具例子；还用重新植入真实旧漏洞的办法自证能查出问题，600 万行 Lean 代码和验证产物都开源了。
需要注意
验证的是代码实现是否符合既定规范，规范本身写错了验证也发现不了；Hacker News 上已有评论质疑，这次查出零个新漏洞，是定理本身写窄了还是只验证了部分性质。