Google made Gemini 4 Carbon, which it calls its strongest model so far, available to paying developers and businesses on 10 November. Until then only a small group of security defenders in Google's Fairwind Program had access, starting two weeks earlier. On the same day, Google DeepMind showed what the model can do on hard engineering work: agents running on Carbon wrote the machine-checked proofs behind a formal verification of libsignal, the reference implementation of the Signal protocol.
The two announcements matter together. One is a new frontier model priced well below its rivals; the other is an early sign that formal verification, long reserved for a handful of projects with years to spare, may become affordable for ordinary software.
What Carbon is and who can use it
Carbon is available through the Gemini API in Google AI Studio and through Gemini for business, and Google AI Ultra subscribers get it in the Gemini app, AI Mode in Search and the Antigravity development platform. The Verge notes it is unclear whether lower tiers or free users will ever get it. Google positions Carbon above Gemini 4 Argon, released a month earlier, for long, multi-step coding, debugging and research, while saying Argon remains the better fit for most everyday engineering. Carbon spends more tokens than Argon to explore and check its own work.
Pricing starts at $2 per million input tokens and $10 per million output tokens, the same introductory rate as Argon. SecurityWeek reports that this lasts until 30 November, after which both prices double. The Verge puts the launch price at about a fifth of OpenAI's GPT-6 Astra and a quarter of Anthropic's Fable 5.2, but cautions that cheaper tokens do not guarantee cheaper tasks, since models use different amounts of tokens for the same job. It also points out that Google's own benchmarks place Carbon behind Fable 5.2 on most measures and that vendors tend to pick favourable results.
Google is also previewing a /swarm command in Antigravity that turns one prompt into a team of coordinated agents. Developers can give Carbon the roles that need the most reasoning, such as architecture and auditing, and pair it with faster models working in parallel, with separate verifier agents testing each change.
Security capabilities stay gated
The general release does not include everything. A version called Carbon for cyber, which Google says leads benchmarks for finding, exploiting and patching vulnerabilities, still requires Fairwind membership. Google cites two early results: Wiz found zero-day flaws at two large SaaS providers in under two hours, and Google's Cloud Vulnerability Research team used the model to show that two bugs in a popular open source project were exploitable, comparable in severity to PHP2Shell, which led maintainers to rate the issue critical and ship a fix. Details will follow once disclosure finishes.
On safety, Google says Carbon blocked 99% of attack attempts by its adaptive red-teaming agent in simulated environments and reached a 0% success rate for attackers on the Gray Swan indirect prompt injection benchmark. Google itself adds that prompt injection robustness still needs work, which is worth keeping in mind before giving any agent access to untrusted input.
Proving Signal's code, not just its design
DeepMind's new framework, AlphaProof Code, pairs human experts with agents. People, working with agents on Carbon and Claude Opus 5.5, turned Signal's security goals into a reviewed Lean specification. Carbon agents then generated the proofs, and the Lean kernel rejected anything invalid. The figures differ between sources: SecurityWeek and The Register report about 6.5 million lines of Lean, while DeepMind's announcement summary says three million.
According to The Register, the work covered Signal's post-quantum PQXDH handshake and the Triple Ratchet, establishing forward secrecy, authentication, post-compromise security and handshake secrecy. SecurityWeek stresses that the guarantees hold for the compiled machine code, where most protocol verification only examines the design. To show the method catches real mistakes, the team reinserted two old, already fixed libsignal bugs and proved that those builds break the guarantees.
The limits are stated plainly. The results apply to Google's own build of libsignal, run through a small command-line wrapper, and "not Signal's own applications". Side channels were left out of parts of the analysis, and The Register notes the proof assumes perfect cryptography. Five researchers needed four weeks, against 20 person-years for verifying the seL4 microkernel. Google is publishing the specifications and proofs.
DeepMind researcher Swarat Chaudhuri told The Register that the hard part is shifting from proving to deciding what to prove. That is the practical takeaway for teams: if machines can produce proofs cheaply, the scarce skill becomes writing precise specifications of what your code must guarantee.
Sources
- Google releases Gemini 4 Carbon with agent ‘swarm’ feature The Verge
- Google Widens Gemini 4 Carbon Access After AI Agents Verify Signal Code SecurityWeek
- Gemini 4 Carbon is now available Google DeepMind
- Google DeepMind melds humans and AI agents to vet Signal's secure messaging techniques The Register
- Introducing AlphaProof Code: a breakthrough in verifying complex software at depth Google DeepMind