Google on Tuesday expanded access to Gemini 4 Carbon and said agents built on the model helped formally verify core security guarantees in the code behind the Signal protocol.
Paying developers and businesses can now use Carbon via the Gemini API and Gemini for business, and Google AI Ultra subscribers are getting access. Introductory rates of $2/$10 per million input/output tokens apply until November 30, then double.
Until now, only select cyber defenders in Google’s Fairwind Program could use Carbon. They still need Fairwind membership for Carbon for cyber, which Google says tops key benchmarks for discovering, exploiting and fixing vulnerabilities.
According to Google, Wiz used Carbon for cyber to find zero-days at two major SaaS providers within two hours. Google’s Cloud Vulnerability Research (CVR) team used the model to confirm that two bugs in a popular open source project were exploitable, with severity comparable to PHP2Shell, a pair of PHP flaws that attackers have already exploited.
“By using Carbon to build a proof of concept, CVR helped maintainers re-classify the bug as critical and swiftly issue a patch,” Google said.
Separately, Google DeepMind introduced AlphaProof Code, which pairs human experts with AI agents to formally verify software, mathematically demonstrating that it meets defined requirements.
The team applied it to libsignal, the Signal protocol’s reference implementation. Versions of the protocol also run in WhatsApp and Google Messages.
Humans worked with agents running on Carbon and Claude Opus 5.5 to write the specifications defining what had to be proven. Carbon-based agents then generated all of the roughly 6.5 million lines of Lean proofs, with Lean rejecting any invalid ones.
The proven guarantees, including forward secrecy, post-compromise security, and authentication, hold for the compiled machine code, while most protocol verification examines only the design.
Five researchers did the proof work in four weeks, something Google says has traditionally taken specialists years.
To show the method catches real flaws, the team reinserted two old, already-patched libsignal bugs and proved that those builds break the security guarantees.
The results cover Google’s own build of the code, run through a small command-line wrapper, and “not Signal’s own applications.” Side channels were also excluded from parts of the analysis.
“The results suggest that AI can make formal verification, historically too expensive for most software, practical for real-world systems,” the researchers wrote.
“As AI-driven security threats grow, rigorously verifying the Signal protocol implementation gives us even greater confidence in our code’s privacy guarantees,” said Signal CTO Ehren Kret.
Google is publicly releasing the specifications and proofs.
Related: Anthropic Rolls Out Mythos 5.2 With Improved Bug Hunting, Fewer Sandbox Escapes
Related: OpenAI Says New GPT-6 Cyber Model Hunts Flaws Without Crossing the Line
Related: OpenAI Model Wrote Its Own Network Code to Get Around Sandbox Restrictions
