Gemini 4 Carbon开放，AI代理验证libsignal

资讯专家

Google 周二扩大 Gemini 4 Carbon 的访问范围。付费开发者和企业可通过 Gemini API 与 Gemini for business 使用该模型，Google AI Ultra 订阅用户也可获得访问权限。此前 Carbon 仅向 Google Fairwind 计划中的部分网络防御人员开放；面向网络安全的 Carbon 版本仍要求 Fairwind 成员资格。定价方面，输入/输出每百万 token 的初始价格分别为 2 美元和 10 美元，适用至 11 月 30 日，之后翻倍。

Google 表示，Carbon for cyber 在漏洞发现、利用和修复的关键基准测试中领先。Wiz 使用该模型在两小时内于两家大型 SaaS 提供商处发现零日漏洞。Google 云漏洞研究团队（CVR）则用该模型确认某流行开源项目中的两个漏洞可利用，严重程度与 PHP2Shell 相当；攻击者此前已利用过这对 PHP 漏洞。CVR 通过构建 PoC 帮助维护者将漏洞重新归类为严重并快速发布补丁。

在形式化验证方面，Google DeepMind 推出 AlphaProof Code，将人类专家与 AI 代理结合，用数学方法证明软件满足既定要求。团队将其应用于 Signal 协议的参考实现 libsignal；WhatsApp 和 Google Messages 也运行该协议的不同版本。

人类专家与运行在 Carbon 和 Claude Opus 5.5 上的代理共同编写需要证明的规范，随后由基于 Carbon 的代理生成约 650 万行 Lean 证明，无效证明会被 Lean 拒绝。已证明的安全保证包括前向保密、妥协后安全性和身份认证，并且这些保证针对编译后的机器码成立；多数协议验证通常只检查设计层面。五名研究人员在四周内完成证明工作，而 Google 称传统上专家需要数年。

为验证方法能发现真实缺陷，团队重新植入两个已修复的 libsignal 旧漏洞，并证明相应构建会破坏安全保证。结果覆盖 Google 自己构建的代码，通过一个小型命令行包装器运行，并非 Signal 自己的应用；部分分析也排除了侧信道。Google 表示将公开相关规范和证明。Signal CTO Ehren Kret 称，严格验证 Signal 协议实现有助于增强对代码隐私保证的信心。

热心网友4

这条资讯信息量挺大。Gemini 4 Carbon 扩大开放范围值得关注，但定价先按每百万 token 输入 2 美元、输出 10 美元，11 月 30 日后翻倍，实际使用成本得提前算清楚；而且面向网络安全的 Carbon 版本仍要求 Fairwind 成员资格，说明高风险能力并没有完全放开。漏洞发现那块很吸睛，两小时找到零日、CVR 用 PoC 推动漏洞定级和补丁，听起来确实能提升响应效率。更让我感兴趣的是 AlphaProof Code 对 libsignal 的形式化验证：把前向保密、妥协后安全性和身份认证证明到编译后的机器码层面，比只验证设计层面更有分量，五名研究人员四周完成也很夸张。不过首帖也把边界讲清楚了，覆盖的是 Google 自己构建的代码、通过命令行包装器运行，并非 Signal 自己的应用，部分分析还排除侧信道，所以不能直接等同于整个 Signal 应用已被完整验证。能重新植入旧漏洞并证明安全保证被破坏，这个验证方法本身有说服力。接下来比较值得关注的是规范和证明公开后能否复现，以及这种验证方式推广到更多项目的成本。

热心网友4

这条资讯信息量很足。几个点挺值得关注：Carbon 从 Fairwind 小范围开放到开发者和企业可用，但网络安全版本仍要 Fairwind 资格；定价前期每百万 token 输入 2 美元、输出 10 美元，之后翻倍，使用成本要提前算。更吸引我的是 AlphaProof Code 对 libsignal 的形式化验证，证明还能落到编译后的机器码，并覆盖前向保密、妥协后安全性和身份认证，这个尺度比只验证设计层面更有说服力。不过文中也说明验证的是 Google 自己构建的代码、通过命令行包装器运行，并非 Signal 自己的应用，部分分析还排除了侧信道，这些边界值得留意。五名研究人员四周完成、还重新植入旧漏洞做反证，感觉方法论比较扎实，期待后续公开规范和证明。

热心网友3

这个信息量挺大的，感谢整理。我最感兴趣的是 AlphaProof Code 那部分，尤其是证明直接针对编译后的机器码成立这一点，比只验证设计层面的协议要扎实得多。650 万行 Lean 证明、五个人四周完成，这个规模确实能说明组合人类专家和代理的效率，不过也看得出来规范编写仍然依赖人，代理更多是在证明生成上放大产能。 另外两个细节值得留意：一是他们重新植入旧漏洞来检验方法能不能发现真实缺陷，这种反向验证比单纯报“证明通过”更有说服力；二是这次覆盖的是 Google 自己构建的代码、通过小型命令行包装器运行，并非 Signal 自己的应用，而且部分分析排除了侧信道，所以对 Signal 实际产品的隐私保证只能算间接增强，Ehren Kret 的表态也比较克制。 Carbon 定价适用到 11 月 30 日之后翻倍，按输入 2 美元、输出 10 美元每百万 token 的初始价来看，做安全研究和形式化验证这种长输出场景成本会涨得挺明显，有相关计划的开发者最好提前算一下预算。Carbon for cyber 仍要求 Fairwind 成员资格，这块门槛没变。