Pricing on one side, proof on the other.
By Ellis Ward | November 11, 2026
Google opened access to Gemini 4 Carbon on Tuesday, making the model available to any paying developer or business. Access now runs through the Gemini API, Google AI Studio, and Gemini for Business. Google AI Ultra subscribers are getting access as well, with rollout extending to Google Antigravity, the Gemini app, and AI Mode in Search.
Until this week, only members of the company's Fairwind Program could use the model. Fairwind was a closed, invitation-based track. Its gates are now open to the broader market.
Pricing during the launch window runs at $2 per million input tokens and $10 per million output tokens. That rate holds through November 30. On December 1, both figures double.
The same day Google widened Carbon access, DeepMind published results from an AlphaProof project that formally verified libsignal. Libsignal is the Signal protocol's reference implementation. The same protocol powers end-to-end encryption in WhatsApp and Google Messages. Five DeepMind researchers completed the work in four weeks. Google says expert teams have traditionally required years to accomplish comparable verification at this depth.
AlphaProof: What It Proved, and What It Did Not
Formal verification is distinct from testing. Testing checks specific inputs. Verification proves, mathematically, that a system satisfies its specification for all possible inputs. AlphaProof's agents did this for libsignal's core security guarantees: forward secrecy, post-compromise security, and authentication.
Forward secrecy means that compromising today's keys does not expose past messages. Post-compromise security means that a compromised session can recover its guarantees once fresh keys are established. Authentication means participants are who they say they are. All three guarantees were proved to hold in compiled machine code, not just at the source level.
That scope matters. Source-level proofs can miss vulnerabilities introduced during compilation or build. DeepMind's proofs reach the compiled binary.
The scope also has limits. The verified build is Google's own version of the code, run through a small command-line wrapper. The proofs do not cover Signal's own applications. DeepMind flags this directly: this is a proof about a specific build, not a blanket certification of Signal as deployed by millions of users.
To stress-test the approach, the team reinserted two old, previously patched bugs into the codebase and ran AlphaProof against those builds. In both cases, the system proved that the modified builds break the security guarantees. The proofs are sensitive to actual vulnerabilities, not passing vacuously on a clean build.
Human Experts, AI Agents, 6.5 Million Lines of Lean
The work paired human experts with AI agents at every stage. Humans working alongside agents running Carbon and Claude Opus 5.5 wrote the formal specifications. Those specs define what libsignal is supposed to guarantee in mathematical terms.
Carbon-based agents then generated the Lean proofs, producing roughly 6.5 million lines according to SecurityWeek. The agents rejected invalid proof candidates as they worked. At the end, the system audited its own output and flagged approximately one percent of the codebase for a second human review. The rest it cleared itself.
Separately, Google's Cloud Vulnerability Research team used Carbon to confirm that two bugs in a popular open source project were exploitable, in a manner comparable to the PHP2Shell vulnerability class.
/swarm, an Open Archive, and Kret's Endorsement
Google also placed /swarm, a multi-agent feature for Carbon, in preview. The setup lets developers assign Carbon to high-level roles: architecture, coordination, and auditing. Faster models handle execution tasks in parallel isolated workspaces. Adversarial verifiers run in separate workspaces and challenge intermediate results.
Google positions Carbon as the stronger model for cybersecurity and long-horizon agentic workflows. For most software engineering and knowledge work, the company recommends Argon instead.
Signal CTO Ehren Kret called the AlphaProof work a major breakthrough. DeepMind is releasing the formal specifications and Lean proofs publicly, which means other researchers can inspect and extend the results.
The two announcements on Tuesday cover different ground. One expands access to a commercial model. The other shows what that model class can do at the frontier of formal methods. DeepMind described it as the first time AI formally verified a widely deployed cryptographic protocol at this depth. After four weeks and 6.5 million lines of proof, the claim holds within its stated scope.
Sources
- SecurityWeek (Nov. 10, 2026): https://www.securityweek.com/google-widens-gemini-4-carbon-access-after-ai-agents-verify-signal-code/
- After Intelligence (Nov. 10-11, 2026): https://newsletter.premarcu.com/archive/edition-068-google-opens-gemini-4-carbon-to-everyone-with-agent-swarms-deepmind-formally-verifies-signal-in-four-weeks-and-a-99-million-parameter-voice-speaks-eleven-languages
