AlphaProof Code
674 points
• 2 days ago
• Article
Link
Google DeepMind 在软件安全领域取得了重大里程碑，成功利用人工智能对 Signal 消息应用程序的核心加密协议进行了形式化验证。这一成就通过一个名为 AlphaProof Code 的新型代理框架实现，标志着在证明代码完全按预期运行且不存在漏洞方面迈出了巨大的一步。过去，形式化验证是一项极其耗费劳动力的任务，但借助这种新方法，研究人员仅用四周时间就完成了对 Signal 广泛部署实现的验证。
AlphaProof Code 框架通过类似专业研究团队的方式来分担验证工作量。人类专家与 AI 合作建立所需的安全规范，而一系列由 Gemini Carbon 模型驱动的 AI 代理则负责创建数学证明这项艰巨工作。该系统生成了超过 600 万行 Lean（为机器校验证明而设计的语言），以确保软件的准确性。通过自动化这一流程，框架让人类专家把注意力放在代码库中只占一小部分、但需要更细致判断的关键环节上，而 Lean 系统则对其余复杂内容进行严格校验。
这一突破尤其引人关注，因为它弥合了协议设计与实际实现之间的难题。尽管许多验证方法停留在高层设计层面，AlphaProof Code 进一步确认：在设备上运行的已编译机器代码始终遵循关键安全属性。团队还通过将已知的历史漏洞重新植入代码来对系统进行再验证，证明 AI 能够成功识别这些版本的问题，并证明其不安全。
随着这项技术走向可扩展应用，未来数字安全的意义也将更为深远：它或将把形式化验证从小众的学术研究，变成保护关键基础设施的可落地方案。凭借数学层面的安全保证，这些方法最终有望应用于保护多类系统，从医疗设备固件到电网软件。与此同时，网络威胁日益复杂，而能够将代码快速核验到具体安全规范之上的能力，将为支撑全球通信的技术提供一条更强有力的新防线。
为推动社区在这一方向开展更深入的探索与开发，Google DeepMind 已将其形式化验证制品开源。该举措旨在促进协作与研究，推动这类由 AI 驱动的安全保障方案在全行业软件加固中的落地实践。通过把自动定理证明与主动防御代理相结合，团队希望在技术快速变革的时代，为构建更具韧性、更安全的系统确立新的标准。
Google DeepMind has reached a significant milestone in software security by successfully utilizing artificial intelligence to formally verify the core cryptographic protocol of the Signal messaging application. This accomplishment, managed through a new agentic framework called AlphaProof Code, represents a major leap forward in proving that code operates exactly as intended without vulnerabilities. Historically, formal verification has been an extremely labor-intensive task, yet this new approach allowed researchers to complete the verification of Signal's widely deployed implementation in just four weeks.
The AlphaProof Code framework functions by splitting the verification workload similarly to a dedicated research team. Human experts collaborate with AI to establish the necessary security specifications, while a series of AI agents, powered by the Gemini Carbon model, undertake the arduous task of creating mathematical proofs. The system generated over six million lines of Lean, a language designed for machine-checked proofs, to ensure the accuracy of the software. By automating this process, the framework allows human experts to focus their attention on the critical one percent of the codebase that requires nuanced judgment, while the Lean system validates the remaining complexity.
This breakthrough is particularly noteworthy because it addresses the difficult gap between the design of a protocol and its actual implementation. While many verification methods stop at the high-level design, AlphaProof Code confirms that the compiled machine code, which runs on devices, consistently adheres to vital security properties. The team further validated the system by reintroducing known historical bugs into the code, demonstrating that the AI could successfully identify and prove these versions were insecure.
The implications for the future of digital security are profound, as this technology moves formal verification from a niche academic pursuit to a scalable solution for critical infrastructure. By providing a mathematical guarantee of security, these techniques could eventually be applied to protect diverse systems ranging from medical device firmware to power grid software. As cyber threats become increasingly sophisticated, the ability to rapidly verify code against security specifications provides a powerful new line of defense for the technologies that underpin global communications.
To encourage further community exploration and development in this space, Google DeepMind has made its formal verification artifacts open-source. This initiative aims to foster collaboration and research into how such AI-driven security assurance can be deployed to harden software across the industry. By combining automated theorem proving with proactive defense agents, the team hopes to establish a new standard for building resilient, secure systems in an era of rapid technological change.
197 comments • Comments Link
• 在此背景下，形式化验证并不能证明不存在所有 bug，而是证明代码行为没有违反由人类专家定义的特定安全模型。
• 验证过程在很大程度上取决于规格说明的质量；如果最初的数学模型存在缺陷，或未能捕获关键的现实世界性质，那么由此产生的证明就会带来一种虚假的安全感。
• 通过针对已编译的 ELF 二进制而非高层 Rust 源码进行验证，验证过程避免了对未经证明且复杂的 Rust 编译器语义的依赖，尽管这只能把保证限定在特定的二进制构建版本上。
• 基于 AI 的工具擅长生成大规模形式化证明，但它们更像是助手而非独立的裁决者：需要人类专家来设定目标、审查逻辑，并应对对抗性边界情况。
• 尽管对"零 bug"的说法仍有人持怀疑态度，但重新引入已知漏洞并确认系统能够检测到它们，表明这一过程具有超越营销噱头的实际效用。
• 由于"停机问题"以及把模糊的现实需求转化为严格且可证明的数学定理所固有的复杂性，将形式化验证扩展到通用软件仍然很困难。
• 有人认为向形式化验证代码的转变是软件工程中不可避免的趋势，类似于行业范围内对加密网页流量的采用；但也有人认为高层业务逻辑仍会抵制这种严谨性。
• 现代开发工作流越来越多地引入专门化的 AI 代理，用来管理长期上下文并协调自主编码任务；在某些团队中，这反而带来了更好的工程实践和更少的线上事故。
• 人们担心这些过程中使用的大语言模型的对齐方式与透明度，尤其是当模型承受的内部压力更偏向基准性能而非可靠性时。
• 当系统一开始就把证明纳入设计时，形式化验证的效果最好；如果试图在混乱的既有代码库上追溯性地"炼成"证明，其效果会差得多。
向 AI 辅助的形式化验证过渡，意味着以更高风险的方式来提供软件安全保障的重大转变，尽管它仍然是用于改进的工具，而不是实现完美万灵药。尽管对像 libsignal 这样复杂库的技术成就令人印象深刻，但讨论也凸显了对基础数学模型局限性以及形式化证明可能无法捕获"规格层"缺陷的健康怀疑。最终，共识是：尽管 AI 能显著降低生成证明所需的工作量，但定义安全优先级并验证逻辑意图这一核心责任依然显然是人类任务。 • Formal verification in this context does not prove the absence of all bugs, but rather that no code behaviors violate the specific security model defined by human experts.
• The verification process relies heavily on the quality of the specifications themselves; if the initial mathematical model is flawed or fails to capture critical real-world properties, the resulting proofs provide a false sense of security.
• By targeting the compiled ELF binary rather than the high-level Rust source, the verification process avoids dependencies on the unproven, complex semantics of the Rust compiler, though this limits the guarantee to one specific binary build.
• AI-driven tools excel at handling the massive scale of formal proof generation, but they act as assistants rather than autonomous arbiters, requiring human experts to frame the goals, review the logic, and handle adversarial edge cases.
• While some skepticism remains regarding the "zero bugs" claim, the ability to re-introduce known vulnerabilities and confirm that the system detects them suggests the process has tangible utility beyond marketing hype.
• Scaling formal verification to general software remains difficult due to the "halting problem" and the inherent complexity of translating ambiguous real-world requirements into strict, provable mathematical theorems.
• The move toward formally verified code is viewed by some as an inevitable shift in software engineering, comparable to the industry-wide adoption of encrypted web traffic, though others argue that high-level business logic will remain resistant to such rigor.
• Modern development workflows are increasingly utilizing specialized AI agents to manage long-term contexts and coordinate autonomous coding tasks, which has paradoxically led to improved engineering practices and fewer production incidents in some teams.
• Concerns exist regarding the alignment and transparency of the large language models used in these processes, particularly when those models are subject to internal pressures that favor benchmark performance over reliability.
• Formal verification is best applied when systems are structured from the start with proofs in mind, as attempting to retroactively "alchemy" proofs onto messy, existing codebases is significantly less effective.
The transition toward AI-assisted formal verification represents a significant shift in how high-stakes software is secured, though it remains a tool for refinement rather than a silver bullet for perfection. While the technical accomplishment of verifying a complex library like libsignal is impressive, the discourse highlights a healthy skepticism regarding the limitations of the underlying mathematical models and the potential for "spec-level" bugs that formal proofs cannot catch. Ultimately, the consensus suggests that while AI can drastically lower the effort required to produce proofs, the core responsibility of defining security priorities and verifying logical intent remains a distinctly human task.