Google DeepMind says AI agents (Gemini Carbon writing Lean) proved key security properties of the actual compiled Signal protocol code, not just the design. Over 6 million lines of Lean, about 1% flagged for human review, done in four weeks. They also put two old, already-fixed Signal bugs back in and the system proved those versions insecure. The proof artifacts are being open-sourced.

Does a machine-checked proof of the implementation change how much you trust an app, or is the spec still the weak spot?

tech

Google DeepMind says AI agents (Gemini Carbon writing Lean) proved key security properties of the actual compiled Signal protocol code, not just the design. Over 6 million lines of Lean, about 1% flagged for human review, done in four weeks. They also put two old, already-fixed Signal bugs back in and the system proved those versions insecure. The proof artifacts are being open-sourced.

Does a machine-checked proof of the implementation change how much you trust an app, or is the spec still the weak spot?