Google DeepMind has used AI agents to verify the actual compiled code behind Signal's encryption, down to the machine-code level. This is a huge step for software security: vulnerabilities can hide in the gap between a protocol's design and the code that implements it. The system, called AlphaProof Code, generated around 6.5 million lines of machine-checked Lean proofs covering key security properties of Signal's handshake and message ratchet. Google says the work took four weeks, a task that could previously have taken expert teams years. The researchers also reintroduced two previously fixed Signal bugs, and the system proved that both broke the specified security guarantees. The proofs cover specific properties under defined assumptions, but this is a remarkable demonstration of how AI could make formal verification practical for real-world software.