pekac

Thrilled to announce that our @GoogleDeepMind team has cracked a major challenge in software engineering and cybersecurity: formally verifying a real-world implementation of the #Signal cryptographic protocol at the machine-code level. This proof was done using AlphaProof Code, our new AI framework for formal specification and verification. * Paper: deepmind.google/documents/36… * Lean code: github.com/google-deepmind/c… * DeepMind blog post: deepmind.google/blog/introdu… A huge shoutout to my amazing teammates: @tchajed, @FerrousAndrew, Jonathan Katz, @pushmeet, @antonkovsharov, Karn Seth, Sam Schlesinger, @RandomlyWalking. I started working on formal software verification 20+ years ago as a grad student. I was persuaded by Dijkstra and other computer science pioneers’ vision of programming backed up by mathematical theorems. At that time, we had to choose between automated code analysis algorithms that scaled but could only prove shallow properties, and deep manual verification that took decades of expert human work. Thanks to progress in AI for mathematical reasoning, we don’t have to make that choice any more. Over four weeks in October 2026, AlphaProof Code agents generated more than 6 million lines of machine-checked Lean proof. We proved deep computational and symbolic security properties of the entire protocol core of Signal, all the way down to the ARM machine-code level. This is just the first step, of course, because our goal is nothing short of verifying the world’s software infrastructure. Most cyberattacks, including the AI-powered ones recently in the news, happen because of preventable code bugs. I expect that agents for formal code analysis will eliminate these bugs one category at a time. As our paper explains in more detail, this doesn’t at all mean humans are out of the picture! Proofs are now largely automated, but human experts will need to decide what is proved with AI assistance. AlphaProof Code offers an early glimpse of what such human-AI collaboration could look like, but many other proposals of this nature will emerge. We have released all our Lean specs and proofs and plan to work with the open-source community on improving them. If you are building critical software and would like to apply these ideas, come talk to us!