来源时间 本站刊期
推出 AlphaProof Code：深度验证复杂软件的重大突破
Introducing AlphaProof Code: a breakthrough in verifying complex software at depth
AlphaProof Code 对安全工程师重要，但形式化验证仍需大量代理劳动。
判断
Signal 安全负责人现在可以权衡在协议发布中采用 AI 辅助形式化验证，但为期四周、超过六百万行 Lean 的工作仍需专家规格说明和对百分之一证明的人工审计，因此应保留给高价值密码学变更，而非例行代码审查。
依据
Signal 首席技术官 Ehren Kret 称，使用 AI 代理将运行中的代码转换为有效的 Lean 定理是“一项重大突破”，并表示严格验证让 Signal 对其隐私保证更有信心。该机制并非单一模型：Google DeepMind 的 AlphaProof Code 将审查每一份形式化规范的人类专家与生成超过六百万行 Lean 的 Gemini Carbon 代理结合起来；随后由 Lean 对证明进行机器检查。代理仅标记百分之一的代码库供人工审计，整个流程仅耗时四周。为测试缺陷检测，团队将两个此前已修复的缺陷重新引入隔离的 Signal 代码库，系统生成了机器检查的证明，表明两个有缺陷版本均不安全。DeepMind 表示，这是首次对广泛部署的密码协议实现进行如此深度的形式化验证。
没写清 来源未说明代理的审计分诊多久会漏掉有缺陷的证明，也未说明百分之一的人工审查切片是否是在未看证明结论的情况下选出的。
下一步 检查开源的 Lean 产物是否包含那两个重新引入缺陷的证明，以及一个可复现、能标记不安全版本的命令。