Google has expanded access to Gemini 4 Carbon and states that agents built on this model helped formally verify core security guarantees in the Signal protocol’s code.
Paying developers and businesses can now use Carbon via the Gemini API and Gemini for business, and Google AI Ultra subscribers also have access. Introductory rates of $2 and $10 per million input and output tokens apply until November 30, before doubling. A token is a unit of text the model processes to read or generate content.
Until now, only certain cybersecurity advocates in Google’s Fairwind program could use Carbon. They must still be part of this program to access Carbon for cyber, a version Google presents as leading in key benchmarks for detecting, exploiting, and fixing vulnerabilities.
Cybersecurity Applications
According to Google, the company Wiz used Carbon for cyber to find ‘zero-day’ type flaws at two major SaaS providers, in two hours. Google’s Cloud Vulnerability Research (CVR) team, for its part, used the model to confirm that two bugs in a popular open-source project were exploitable, with a severity comparable to that of PHP2Shell, a pair of PHP flaws already exploited by attackers.
‘By using Carbon to build a proof of concept, CVR helped the maintainers reclassify the bug as critical and quickly publish a patch,’ Google states.
Verifying Signal’s Code
Separately, Google DeepMind introduced AlphaProof Code, which combines human experts with AI agents to formally verify software, i.e., mathematically demonstrate that it meets defined requirements. The team applied it to libsignal, the reference implementation of the Signal protocol. Versions of this protocol also operate in WhatsApp and Google Messages.
Humans worked with agents running on Carbon and on Claude Opus 5.5 to write the specifications describing what needed to be proven. Agents based on Carbon then generated the entirety of the approximately 6.5 million lines of proofs written in Lean, a proof assistant that rejects invalid ones. According to Google, the proven guarantees, including forward secrecy, post-compromise security, and authentication, apply to the compiled machine code, whereas most protocol verifications only concern the design.
Five researchers completed the proof work in four weeks, a task Google estimates is traditionally reserved for specialists over years. To verify that the method detects real flaws, the team reintroduced two old bugs in libsignal, already fixed, and proved that these versions no longer meet the security guarantees.
The results pertain to the version of the code compiled by Google, executed via a small command-line tool, and not to ‘the Signal applications themselves.’ Some side channels were also excluded from parts of the analysis. ‘The results suggest that AI can make formal verification, historically too costly for most software, feasible for real-world systems,’ the researchers write. Ehren Kret, Signal’s CTO, stated: ‘As AI-related security threats multiply, rigorous verification of the Signal protocol implementation gives us even greater confidence in the privacy guarantees of our code.’ Google is also publishing the specifications and proofs.
