# Google uses Gemini 4 Carbon to formally verify Signal protocol code

> Original title: Our teams put Gemini 4 Carbon to work on a major security challenge: mathematically proving the code underlying the Signal protocol.

- Source: Sundar Pichai
- Published: 2026-11-10T17:28:49.000Z
- Bad Influence: https://badinfluence.news/items/iil5ij1msksgz2igzay1wkplk
- Original: https://x.com/sundarpichai/status/2120207062655549933

## Summary

Google says its teams used Gemini 4 Carbon and AlphaProof Code to formally verify the code underlying the Signal protocol, down to compiled device code. The effort produced over 6M lines of machine-checked Lean proofs, with about 1% of the codebase requiring human review. Google says it is open sourcing the results for the security community.

## Post

Our teams put Gemini 4 Carbon to work on a major security challenge: mathematically proving the code underlying the Signal protocol.

Using AlphaProof Code, @GoogleDeepMind researchers guided agents to verify the protocol down to compiled device code, closing the gap where real bugs hide. The result:

- Gemini 4 Carbon generated over 6M lines of machine-checked Lean proofs
- years of expert manual verification compressed to just weeks
~1% of the codebase required human review (Lean automatically checked the rest)

This is helping unlock scalable formal verification for building secure software, laying the groundwork to fundamentally shift the advantage to defenders. We’re open sourcing the results for the security community.

![](https://badinfluence.news/api/img-proxy?u=https%3A%2F%2Fpbs.twimg.com%2Fmedia%2FHWx77X5bMAAjBvx.jpg&mode=thumb&exp=1794528000&sig=1dbb7eb9e87f56c9)