四周验证 Signal 代码，AI 形式验证迎来新突破

据 Woofun AI 消息，Google DeepMind 于 11 月 10 日在官方部落格发布 ，首次利用 AI 对 加密协定进行深度形式验证，证实其装置端实际执行的代码符合专家设定的主要安全性质。

这次突破的核心在于验证深度的根本性跨越。传统的形式验证多局限于设计层面，仅能证明"设计"本身的安全，而真实世界的漏洞往往隐藏在设计与实作之间的落差。AlphaProof Code 则一路证明到编译后的代码，例如验证装置暂时被入侵前后讯息仍受保护等性质，将证明难度大幅提高。

Woofun AI 整理数据显示，整个验证过程仅耗时四周，而传统专家团队完成同等深度验证通常需要好几年时间。具体执行上，AlphaProof Code 采用人机协作模式：人类专家与 AI 共同决定"要证明什么"，并将 Signal 的安全目标转化为形式化的数学规格，每一条规格均经人类专家审核。随后，由 驱动的 AI 代理接手证明工作，写出超过 600 万行 代码。Lean 是一种用于撰写数学证明的程式语言，电脑可自动检查每一步逻辑。最后，代理自行稽核证明，标出仅占整体 1% 需要人类再次审查的部分，其余均由 Lean 自动检查，使专家能专注于真正需要判断的关键环节。

为验证系统的有效性，研究人员在隔离环境中将两个已修好的旧漏洞重新植入 Signal 代码，系统两次均产出经机器检查的证明，准确指出有漏洞的版本不安全。Signal 技术长 在部落格中评价，过去形式验证涵盖范围有限，确认正式上线代码严格符合加密设计需大量人工，而用 AI 代理将线上代码自动转为有效 Lean 定理是"很大的突破"。他指出，面对日益增加的 AI 驱动网络安全威胁，核心协定经过严格验证让 Signal 对自家代码的隐私保证"更有信心"。

目前，DeepMind 已将形式验证成果开源并附上技术论文，并表示同一套方法未来可应用于医疗设备韧体、电网软件等关键系统，但扩大规模仍需更多研究。

业界对 AI 辅助形式验证的关注正迅速扩大。 于 10 月与 合作，利用 形式验证 123 个开源函式库，过程中发现数百个错误。以太坊共同创始人 在 Devcon 8 开幕演讲中亦强调，应以开源、可验证取代单纯信任，并点名芯片、通讯、AI 等领域皆需具备可验证性。这标志着形式验证正从理论验证走向大规模实作验证的关键转折点。