On 10 November, Wired reported that Google DeepMind researchers had used an AI framework called AlphaProof Code to formally verify several cryptographic guarantees of the Signal Protocol in a four-week project. The protocol protects communications in Signal, Google Messages and WhatsApp.
Formal verification starts by expressing what software must do as mathematical statements, then proving that those statements hold. Writing the statements and developing the proofs has historically taken substantial human effort. DeepMind’s framework uses AI agents to help develop the proofs, while people still provide input and review.
Sending a private message could depend on the guarantees examined in this project. The researchers analysed portions of the protocol, however, rather than formally verifying the entire Signal mobile app.
The researchers found no new vulnerabilities in the portions they examined. Applied to older versions containing known, long-fixed flaws, AlphaProof Code identified those flaws and could not verify the protocol. DeepMind researchers said earlier verification work by the Signal Foundation gave their project a head start. They are releasing their specification and proof to support further verification work.
