谷歌刚刚利用人工智能代理对 Signal 协议进行了形式化验证。 这不是设计文档。 而是用于保护 Signal 和 Google Messages 消息的实际代码。 DeepMind 的 AlphaProof 代码代理（由 Gemini Carbon 提供支持）编写了超过 600 万行精益代码。 精益代码是用于从数学角度证明代码正确性的语言。 验证过程耗时 4 周。 DeepMind 表示，以往这类工作通常需要专家团队花费数年时间。 他们甚至故意重新引入了两个已修复的旧漏洞。系统证明这两个版本都不安全。 Signal 的首席技术官称之为一项重大突破。 如果您关注加密、隐私或真正值得信赖的代理，那么这就是本周的新闻。 形式化验证会成为主流，还是只是昙花一现？