Google DeepMind researchers used the AlphaProof Code framework to machine-check security guarantees in compiled machine code for the Signal Protocol, extending earlier analyses that focused on the protocol’s design.

A five-person team completed the work in about four weeks, using AI agents to produce roughly 6.5 million lines of Lean proof covering around 140,000 AArch64 instructions; researchers guided the process and reviewed flagged sections, and Google did not disclose the computing cost.

That timeline is striking beside earlier formal-verification efforts: verifying the seL4 microkernel took 20 person-years, while developing the verified CompCert C compiler took six years.

The team also tested older Signal builds by reintroducing two previously patched bugs, and the verification correctly showed that those builds failed to meet the stated guarantees.

The proof system accepted results only after Lean’s kernel checked them against a human-approved specification, with proposed changes to trusted assumptions subject to human approval or policy controls and logging.

AI agents helped generate and refine the proofs, but people still had to decide which properties mattered and specify what the system must prove.

The claims are bounded: symbolic results assume perfect cryptography, while the separate computational argument applies only within its attacker model and does not establish the secrecy of actual message bytes in every circumstance.

The guarantees cover the core protocol implementation under the study’s assumptions, not side channels or the rest of the messaging app; formal verification also does not replace fuzzing, penetration testing, dependency checks or operational monitoring.

The project remains research rather than a commercial cybersecurity product, although DeepMind has released its verification artifacts for public inspection and further work.

Researchers see specification as a central hurdle to expanding the approach: humans must clearly define what software should and should not do before agents can generate proofs against it.

Swarat Chaudhuri called the result a milestone but cautioned that applying the method across software at global scale remains a long-term goal; Pushmeet Kohli pointed to potential uses at banks and other companies.

Google DeepMind hopes to apply verification beyond cryptographic protocols, including to systems such as medical-device firmware and power-grid software, while the affordability and practicality of scaling it to large codebases remain unresolved.