A proof about code, not just a design

Google DeepMind published a paper on November 10 describing how its AlphaProof Code system helped verify parts of libsignal, the reference software for the Signal messaging protocol. The authors report that a compiled build met specific security requirements for starting an encrypted session and for updating encryption keys as messages are exchanged.

A protocol tells programmers how the exchange should work. The implementation is the code that actually does it. A mathematical argument about the design can miss a mistake in the code. The researchers checked instructions compiled from unmodified library source for 64-bit Arm Linux, using a small command-line program to run the library.

What the AI did and what Lean checked

Researchers and AI agents turned security goals into precise statements. People reviewed those statements. Other agents wrote proofs, which Lean, a proof-checking system, checked against the agreed statements. An agent’s confidence in its answer was not the test.

The team also put two previously fixed bugs back into isolated builds. It reports that the verification showed those builds violated the security requirements. That is a check that the specifications can catch real mistakes of those kinds, not a search that rules out every other bug.

Where the assurance ends

The claims depend on how the researchers modelled the processor, the assumed security of underlying cryptographic tools and the behaviour specified for some routines. They concern the parts of the library that were checked. They do not establish that the whole app, every platform build or every device using it is secure.

DeepMind has made the proof materials available for scrutiny. The next questions are whether others can reproduce the work and how easily it can be kept current as the library changes.

Sources

  1. Google DeepMind: Introducing AlphaProof CodeNovember 10 announcement and developer account of workflow, scope and historical bug checks.
  2. Chaudhuri et al.: AlphaProof Code technical paper and artifactsPaper and artifacts. Sections 4–6 specify the AArch64 Linux binary, assumptions, proved properties and historical bug exercises.