软件安全，终于开始追问机器真正执行了什么
一款通讯软件每天处理大量私人消息，人们相信它的加密协议，却很难看见协议之下的实现究竟经历过多少次编译、优化和版本迁移。密码学论文证明的是理想模型中的性质，安全团队审计的是源代码，真正运行在设备上的则是一串机器指令。这几层之间只要出现偏差，严谨的理论也可能被工程细节拖累。11月10日，Google DeepMind公布AlphaProof Code研究，选中的对象是Signal协议参考实现libsignal的关键代码。团队让智能体承担大规模形式化证明生成，由人类审定规范，再由Lean的证明内核逐项核验，将安全性质连接到AArch64机器代码。对于习惯依赖测试覆盖率、扫描报告和渗透测试的研发团队，这份工作提供了另一类质量证据：软件的指定关键性质能够写成数学命题，再由机器检查完整证明过程。
官方技术材料披露，研究生成约650万行经Lean检查的证明代码，依赖约2.6万行可信规范和AArch64语义定义。研究由五名人员在四周内并行完成，并通过重新引入两处过去已修复的缺陷，检查规格是否能暴露安全问题。这些数字的价值并不来自“AI写了多少行”，而是复杂软件中的一部分验证劳动开始可以分工：专家定义规格，智能体扩展证明，形式化内核严格复查。研究者将技术论文及证明工件公开，使这件事有了可供同行核实的工程对象。
从协议模型到机器指令，跨过最难的一座桥
理解这次工作的意义，可以想象一座桥梁的设计与施工。设计人员证明结构在既定载荷下符合要求，但施工中出现材料替换、连接变化或者几何偏差，结论需要重新检查。软件同样如此。协议专家讨论前向保密、消息机密性、身份认证和系统遭到攻陷后的恢复能力，工程师却必须处理内存分配、函数调用、寄存器、编译优化和目标平台。仅有协议层的正确性，很难对最终发布的二进制承担完整责任；大量测试也无法穷尽密码学意义上的攻击交互。AlphaProof Code试图缩短这种断层，让抽象安全性质和真实代码之间建立可追溯的证明关系。
研究将已有符号模型和计算模型引入Lean，在人类指导下补足协议版本、握手与密钥棘轮之间的联系，再对实际编译代码建立形式语义。论文报告的结论覆盖指定范围内的前向保密、攻陷后安全性、消息机密性与真实性；量子攻击相关的部分也限定在特定模型中。证明触及编译后的机器代码，让工程团队能进一步核对证明对象与交付对象的对应关系。整套应用的其他组件仍在本次验证范围之外。
Lean不负责灵感，它负责拒绝不合规则的推理
大语言模型擅长组合已有知识、搜索证明路线与分解复杂问题，也可能在看似流畅的逻辑中遗漏前提。形式化验证解决这一问题的方式很朴素：把推理步骤放进严格的类型和逻辑系统。Lean是交互式定理证明语言，规范、引理和最终定理都必须被明确写出。证明作者可以是数学家、工程师或智能体，但能否成立，取决于内核认可的推理规则。智能体可以尝试多条路径、失败后重试，无法用自然语言上的自信替代一个通过检查的证明对象。
于是，研究的关键结构是人机分工。规范为什么这样定义、攻击者被假设拥有哪些能力、哪些系统边界被包含、哪些组件被信任，仍需要人类专家负责。证明搜索则适合并行和自动化。这样的模式很像制造业由工艺工程师制定验收标准、自动化设备执行工序、计量系统核对结果。AI让某些繁重劳动的成本下降，验收依据却必须独立于生产者。未来智能体做代码审计、工业仿真和参数配置，都可以沿用这条原则。
证明代码很多，可信计算基础反而要尽量小
把“650万行”孤立看，很容易误以为研究只是在验证环节又制造了更大的代码山。形式化证明通常需要大量重复而细碎的中间推导，机器可以检查这些步骤，人类却不需要逐行主观相信。真正需要审查的是被证明的命题、硬件指令语义、代码对应关系以及外部假设。论文特别区分证明总代码与可信规格规模，就是在说明这层边界：大规模劳动能够自动完成，而需要人类承担信任责任的部分仍应受到严格约束。
企业软件还要考虑库文件、编译器、驱动、操作系统、通信链路和运行配置。某个加密模块获得证明，并不代表身份系统、密钥管理、供应链或设备运维同时安全。对于工控设备，即使通信实现足够严谨，PLC程序下载权限、远程维护账户、工程站补丁和错误的网络分区仍可能形成风险。数学证明增强的是特定范围内的确定性，真正可交付的安全结论必须写清其适用版本、假设、未覆盖对象和可信部件。企业最需要警惕的，是让一份漂亮的证明报告变成对全系统的过度承诺。
重新植入两个旧漏洞，是比演示成功更有力的测试
一套形式化体系可能陷入另一个陷阱：证明完全正确，规格却漏写了真正重要的安全要求。如果规格过于宽松，有缺陷的程序同样能够符合要求。因此，团队将两个过去已修复的libsignal缺陷重新引入目标代码，检查系统能否发现相应的安全违背。研究报告显示，这些缺陷使相关二进制违反了所建立的符号安全定理。这个实验设计让规格本身接受部分反向检验：不仅证明好的实现应当通过，也要让已知错误被挡下。它提供了强于单纯成功演示的说服力，但仍只是针对已知问题的验证，无法代表未来所有未知错误。
工业研发中常见类似问题。团队喜欢展示异常检测模型在正常工况下运行顺畅，却没有把历次误操作、设备故障、工艺越界和错误审批整理成可以重复运行的负面样例。历史事故、MES错误工单、关键参数超限、检验放行失误，都应当转化为验证系统必须识别的场景。智能体能够生成方案和报告以后，测试集除了覆盖成功结果，还要覆盖故障恢复、权限拒绝、相互冲突的指令与人工接管。经得起故意“找茬”的工程系统，才可能进入严肃的生产环境。
把形式化验证带进工业现场，应该从小而关键的模块开始
工厂不会因为一项研究突破就马上把控制系统交给智能体。连续化工装置的紧急停车逻辑、电力系统保护程序、重型装备的固件升级和工业通信协议，都具备故障代价高、审核责任明确、服役周期长的特点。另一方面，这些关键任务中的某些子模块边界非常清晰，适合逐步采用形式化方法。企业可以先识别状态机转换、身份与权限校验、固件签名验证、关键通信会话或故障安全逻辑，对这些模块建立规格、测试和证据包，再逐渐扩展到跨模块行为。
产品交付需要至少三类能力。首先是规格管理，把工程要求、标准条款和历史问题转化为版本化的机器可读条件，并留下批准记录。其次是验证代理，从源码、模型和编译产物中调用工具，生成证明或反例，保留每一次修改和失败原因。最后是交付审查，把验证范围、假设条件、未覆盖部分、内核版本和二进制哈希整理为复核材料。客户需要的是能够对应实际固件版本、供第三方审计的证据，不是一张“AI验证通过”的宣传截图。对数据不出厂的场景，这些验证工具还要能够在本地网络运行。
代码代理下一轮竞争，可能发生在验证和认证环节
过去企业评价AI编程，多围绕生成速度、代码数量和开发者效率。随着代理开始承担越来越长的修改任务，一个新的问题变得突出：自动生成的变更如何以可控风险进入生产系统？在医疗、能源、轨道交通等领域，修复缺陷的真实成本可能远高于写出补丁；功能测试通过之后，质量审查、系统集成、认证和客户签署仍占用大量精力。如果形式化工具降低了关键模块获得严格证据的门槛，软件交付中的验证与沟通过程就有机会被重塑。
商业化路径应当按风险分层。普通应用继续采用单元测试、集成测试和静态分析，高风险权限或加密功能增加模型检查与定理证明，极关键的代码链路再投入机器代码级验证。供应商要根据规格稳定性、证明复用率、算力消耗和维护工作量定价；客户则结合事故风险、停机损失和认证周期评估收益。证明程度越高，成本通常越高，投入应与系统风险相称。真正值得付费的地方，往往不是代码最多的业务，而是错误后果最严重的环节。
证明能够生成，证明如何长期维护才刚刚开始
工业软件的寿命常常以十年计，而编译器、处理器、协议版本和供应链一直在变化。如果一次验证消耗大量计算，下一次小范围修改能否进行增量证明？如果更换目标芯片，指令语义、内存模型与编译配置如何迁移？如果证明失败，开发者能否定位到某个接口、定义或编译选项？这些都是工程推广必须回答的问题。企业需要的不是一项永远停留在实验室里的重大成果，而是能被持续集成工具调用、可以管理版本并且费用可预测的验证服务。
真实设备还有并发、实时性、侧信道、外设行为、硬件故障和物理环境等因素。指定密码学性质在给定攻击模型下成立，不会自动覆盖所有安全威胁。另一方面，形式化证明也不应该被要求独自解决整个世界的风险。正确的方法是把它融入分层工程体系：单元测试验证功能，仿真验证行为边界，安全分析检查威胁路径，形式化工具负责能够准确建模的关键性质，现场试验再处理模型与现实之间的差距。每一种证据都有自己的强项和局限，组合之后才形成可信交付。
从工业智能体到工业智能算网，要把证据当成产品资产
工业智能体未来会调用CAD、CAE、PLM、MES与现场数据，生成工艺路线、参数调整建议、设备维护报告，甚至协助修改工程配置。这样的系统若只评价“生成得像不像专家”，很容易漏掉工程约束。工业AI工作台应把专业约束、工具执行和验证证据分别留存。专业约束库管理设备手册、图纸参数、工艺窗口与安全规则；执行库负责外部软件接口、权限隔离、只读优先和审计；证据库则把仿真结果、测试记录、规则检查与人工签署关联到每次输出。形式化证明是其中一种最高强度的验证方式，物理计算、数据一致性和现场试验同样不可缺少。
AlphaProof Code的冲击，是让复杂软件中的部分“可信”开始具备可交付、可移交、可再次核查的形式。未来人们评价智能体时，或许会少问它生成了多少代码，而更多追问任务完成后留下了怎样的证据。对于工业软件产业，这条路线值得持续关注：让AI承担更多劳动，同时将每一个高价值结论落实到明确的规格、版本和验证结果之上。研究还在推进，证明覆盖范围、产业成本及独立复现情况都需要继续观察；但软件质量从“相信生产者”走向“核验交付物”的方向已经更加清晰。
一个可操作的企业验证试点
如果一家装备制造企业准备在一年内开展试点，可以从升级包签名校验或远程维护身份模块开始。首先组织软件、安全和设备三类人员共同识别失效后果，明确哪些条件可以由形式化语言准确表达；随后冻结一份样例代码与构建配置，按“规格编写—自动证明—反例分析—人工复核”循环推进，并刻意注入历史缺陷测试检查系统能否拒绝错误实现。验收报告应列出人工编写规格所耗工时、代理计算开销、覆盖的版本、发现的缺陷和仍未证明的部分。下一阶段再让编译器或依赖库发生受控变化，测量证明能否重复使用。这样的试点即使范围不大，也能为企业决定是否扩展投入提供客观依据，而非依赖概念演示。
参考资料
- Google DeepMind，Introducing AlphaProof Code: a breakthrough in verifying complex software at depth，2026-11-10。https://deepmind.google/blog/introducing-alphaproof-code/
- Chaudhuri等，AlphaProof Code: Verifying Signal’s Security at the Machine-Code Level，论文及证明工件，2026-11-10。https://google-deepmind.github.io/code-verification/
- Google DeepMind，验证代码仓库。https://github.com/google-deepmind/code-verification