Google DeepMind has succeeded in mathematically verifying the core software of encrypted messenger Signal down to machine code level using an AI agent. It also checked security in the compiled output of the actual program, drawing attention.

On Nov. 12 (local time), Taiwan media outlet IT Home reported that DeepMind released the AlphaProof Code, an AI-based formal verification framework, and said it verified libsignal, a core library of the Signal encryption protocol.

Formal verification is a technique that mathematically defines the security conditions a program must satisfy and then proves that the actual code meets those conditions. While previous research mainly focused on protocol designs or modified code, this time the verification targeted unmodified, real implementation code.

The research team connected Rust-based libsignal to a command-line test program and compiled it into AArch64 Linux machine code. It then mathematically analyzed the machine code’s execution behavior to confirm it met the specified security requirements.

Five researchers worked with an AI agent for four weeks to write about 6.5 million lines of Lean proof code. After people reviewed and approved the security requirements, a Gemini Carbon-based AI agent generated proofs, and the Lean verifier checked mathematical validity.

The verification targets included PQXDH, which negotiates initial encryption keys, and the Triple Ratchet, which updates keys during message exchanges.

The team verified forward secrecy that protects past communications, message authentication, and conditions for recovering security after some encryption keys are leaked.

It also tested error-detection capability. After reinserting 2 previously fixed vulnerabilities into a test program, it mathematically proved in both cases that the specified security conditions were violated.

The verification does not guarantee the safety of the entire Signal app. It is limited to a test program using a specific version of libsignal and does not cover group chats, multi-device environments or all quantum-computer attacks.

The safety of some cryptographic operations is also based on assumptions. DeepMind released the related proofs and code and suggested the technology could be used in the future to verify security for key systems such as medical devices and power grids.