Two things from Google today. Gemini 4 Carbon is now open to paying developers, businesses and AI Ultra subscribers, at $2/$10 per million input/output tokens until November 30, then double. The cyber version still requires Fairwind membership.
The Signal proof
The bigger story to me is AlphaProof Code. Five researchers paired with agents running on Carbon and Claude Opus 5.5 to formally verify libsignal, the reference code behind Signal and versions of WhatsApp and Google Messages. Claude helped write the specs. Carbon agents generated around 6.5 million lines of Lean proofs, and Lean threw out the bad ones. Guarantees like forward secrecy and post-compromise security were proven on the compiled machine code. It took four weeks, a job that traditionally takes specialists years.
To prove the method catches real bugs, they put two old libsignal bugs back in and showed those builds failed.
Fine print
It covers Google’s build of the code, not Signal’s apps, and side channels were excluded in places. Still, if AI makes formal verification cheap, that’s one of the best things AI could do for security. Google is publishing the specs and proofs.
God Bless, and Use the Source!
