What changed
Google DeepMind released AlphaProof Code, a human-guided multi-agent framework that generated about 6.5 million lines of Lean proofs for libsignal's compiled AArch64 implementation. The checked scope covers PQXDH and Triple Ratchet properties including authentication, forward secrecy, post-compromise security and handshake secrecy.
Why it matters
The work applies AI agents to implementation-level assurance rather than prose review or test generation. Lean's kernel checks every accepted proof, while humans remain responsible for the specification and trusted semantics.
What to do
Security teams should inspect the open specifications and trusted assumptions before reusing the method on one narrow critical routine. Treat any proved property as only as broad as the approved specification, compiler path and modeled architecture.
Caveat
DeepMind calls this a breakthrough, but the result assumes cryptographic primitives and trusts roughly 26,000 lines of specifications and AArch64 semantics. It does not prove Signal has no bugs, cover every platform or remove the need for expert specification review.