AI agents mathematically prove Signal's implementation
Google DeepMind announced "AlphaProof Code," a new framework for formal verification of software, on Nov. 10 (Nov. 10 Japan time). Formal verification is a method of mathematically proving that a program always satisfies specified properties, and it is considered the most rigorous way to guarantee software security. Under the guidance of the company's researchers, AI agents proved key security properties of the actual code of the Signal Protocol, the company said. The Signal Protocol is the cryptographic system that protects conversations in the messaging app Signal and in Google Messages.
According to the technical paper released at the same time, the target was "libsignal," the reference implementation of the Signal Protocol, and the proofs were done at the level of compiled machine code (AArch64). The proofs cover two parts: "PQXDH," a post-quantum procedure for sharing keys at the start of a conversation, and the "Triple Ratchet," which updates keys with each message. The four properties are forward secrecy, which prevents past communications from being decrypted later; authentication of the other party; post-compromise security, which returns to a secure state after a key is temporarily leaked; and the secrecy of key exchange.
DeepMind said in its blog that this is the first time a widely used cryptographic protocol has been formally verified at this depth using AI. It also said this is the first time an implementation of such a widely used protocol has been formally verified by any method, with or without AI. The paper says it is the first proof that connects protocol-level security guarantees to the unmodified code of a widely used cryptographic protocol implementation.
AI handles the proofs, humans check the specifications
According to the blog, AlphaProof Code uses multiple AI models; humans and AI decide what to prove, and a swarm of AI agents carries out the proofs themselves. The specifications (the properties to be proved, written as mathematical formulas) were created by researchers working with multiple models, and human experts checked all of them. The proofs were handled by agents using "Gemini Carbon," which generated more than 6 million lines of code in "Lean," the language in which the proofs are written, the company said. The agents audited the proofs, and the parts they flagged for human review made up only 1% of the codebase; Lean automatically checks the rest.
The paper says agents using Gemini 4 Carbon and Anthropic's "Claude Opus 5.5" were used to create the specifications, while the proofs were produced solely by a swarm of agents using Gemini 4 Carbon. The authors did not write a single line of the proof code, it says. At the same time, it says most of the work was spent on creating the specifications rather than the proofs.
The blog put the verification time at "just four weeks," describing it as work that previously took teams of experts years. According to the paper, those four weeks were the work of a team of five, which pursued two types of proofs in parallel. One is a "symbolic model," which treats cryptography as idealized components, and the other is a "computational model," which bounds the probability of a successful attack by computational hardness. As past examples, the paper notes that verifying "seL4," the core of an operating system, took 20 person-years, and the C compiler "CompCert" took six person-years. Both were code written with verification in mind, it says.
About 6.5 million lines of proofs
According to the paper, the Lean code in the published repository totals about 7 million lines, including comments and blank lines. Of that, the proofs account for about 6.5 million lines: 5.3 million lines of proofs about the executable's behavior, about 860,000 lines for the computational model and about 350,000 lines for the symbolic model. The libsignal code verified amounts to about 560KB, or about 140,000 AArch64 instructions.
Because Lean mechanically checks the correctness of the proofs, the paper explains, what people need to check to trust the result is the specification side. The abstract puts the trusted specifications and AArch64 semantics together at about 26,000 lines.
The target is an executable run from a CLI, with cryptographic components treated as assumptions
The blog said that while many protocol verifications stop at the design level, this one proved properties all the way down to the code running on devices. The properties covered include protecting messages before and after a device is temporarily compromised, it said.
The scope of verification shown in the paper and the public repository is narrower. Unmodified libsignal (v0.105.4) was connected to a small command-line (CLI) program and compiled into an executable for AArch64 Linux with the standard Rust compiler (rustc 1.98.1). The proofs concern the machine code of this executable. Low-level cryptographic operations such as SHA-256, AES and elliptic-curve arithmetic, as well as some memory operations and file writes, were treated as behaving according to predetermined conditions.
The paper says the work covers only one-to-one conversations, with group messaging left for future work. Key generation was not verified, and side-channel attacks, which seek secrets from factors such as processing time, are also out of scope.
Two reintroduced known bugs detected
To test whether the method could tell correct code from buggy code, DeepMind reintroduced two real bugs that had previously been fixed into an isolated version of the code. In both cases, it showed with machine-checkable proofs that the buggy version was insecure, the company said.
According to the paper, both bugs had been found in libsignal by researchers including Cheval and had already been fixed. DeepMind recompiled the code with the fixes reverted and proved in Lean that the resulting executable does not satisfy the security theorems.
Signal's chief technology officer calls it "a major advance"
Ehren Kret, chief technology officer (CTO) of Signal, said in a comment in the official blog that using AI agents to turn actual running code into correct Lean theorems is a major advance. Amid growing AI-driven security threats, the rigorous verification of the Signal Protocol gives even greater confidence that the code delivers on its privacy guarantees, he said.
DeepMind released the formal verification artifacts. The GitHub repository contains both the symbolic model and computational model proofs, and DeepMind's code is provided under Apache 2.0. The libsignal code included in the repository remains under its original AGPL-3.0 license.
The company said it will apply the work to securing other critical systems, such as firmware for medical devices and software for power grids. On Nov. 6, DeepMind also published research in which AI agents found two weaknesses in legacy 1024-bit RSA.
