Congrats to DeepMind on their achievement! BAIF launched Signal Shot in Apr 2026, and we are excited to see quick progress on the use of AI tools and the Lean theorem prover towards the verification of a critical complex software system like the Signal Messenger.
Google DeepMind’s achievement connects Lean-checked symbolic and computational proofs of key security properties of PQXDH and the Triple Ratchet, including its Double Ratchet component, to a specific AArch64 Linux binary built from libsignal. The correctness of the SPQR component of the Triple Ratchet and of the cuirve25519-dalek cryptographic primitives were assumed.
At BAIF, our work on Signal Shot includes end-to-end verification of PQXDH and SPQR from the protocol models to the Rust implementations, using Aeneas to translate Rust into Lean. We are also developing the secure-messaging library, built on the existing VCVio framework. We develop reusable protocol models and security games for many artifacts. Examples are SCKA constructions, such as ML-KEM Braid. Full Double and Triple Ratchet composition. They are among BAIF’s broader programme’s goals.
Our PQXDH specification work in collaboration with Galois, models the PQXDH protocol as an instance of a reusable UAKE framework, unilaterally authenticated key exchange, following Dodis and Fiore, with explicit scheme definitions and associated security games. DeepMind’s computational PQXDH formalization follows a different specification route, drawing on Rune Fiedler and Felix Günther’s Security Analysis of Signal’s PQXDH Handshake and Bhargavan et al.’s CryptoVerif analysis. Their achievement overlaps with our work in protocol coverage, but the particular UAKE specification framework we are developing is a distinct contribution.
The main complementarity is between source-level and binary-level verification. Our source-oriented proofs express implementation behaviour through the Rust functions and types that developers maintain; DeepMind’s work connects high-level specifications to the compiled AArch64 instructions, including their calling conventions and memory layouts. Comparing and aligning the specifications could provide useful cross-checks between these two levels. We hope that sharing specifications, proof infrastructure and results will strengthen the verification of Signal and benefit the wider open-source community.
What is still remaining to do:
Multiple other protocols used in Signal which weren’t formalised or proven in this project (e.g. SPQR, SCKA, KVAC).
AArch64 semantics were created during the project and are part of the trust base (they are machine checked with differential testing) and are part of their trust base.
Anonymous Credentials: This part of libsignal has not been formalized by Deepmind. We are formalizing the most updated version of Signal's anonymous credential system (muCMZ). We formally specify the protocol and prove security properties of the protocol and code with respect to the formalization.
No process for continuous verification being included within the usual workflow of the software engineering process
Moving ahead, there is still a lot of work to be done. Besides formalization and verification of remaining components, Signal Shot’s original goals include developing continuous verification workflows. We will continue to build open scalable tools that benefit the larger cryptography community and Rust software engineers.