--- title: DeepMind's 6.5M lines of Lean proofs make verification cheap description: Google DeepMind says a five-person team formally verified Signal's messaging security in four weeks, compared to the 20 person-years it took for the seL4... canonical: https://daily.dev/posts/deepmind-s-6-5m-lines-of-lean-proofs-make-verification-cheap-zcfmcbgmv twitter:card: summary_large_image twitter:site: @dailydotdev og:type: website og:site_name: daily.dev og:title: DeepMind's 6.5M lines of Lean proofs make verification cheap | daily.dev og:description: Google DeepMind says a five-person team formally verified Signal's messaging security in four weeks, compared to the 20 person-years it took for the seL4... og:url: https://daily.dev/posts/deepmind-s-6-5m-lines-of-lean-proofs-make-verification-cheap-zcfmcbgmv og:image: https://api.daily.dev/og/posts/zcFMCbGmV.png og:image:alt: DeepMind's 6.5M lines of Lean proofs make verification cheap og:image:width: 1200 og:image:height: 630 og:locale: en --- > ## Documentation Index > Fetch the complete documentation index at: https://daily.dev/llms.txt > Use this file to discover all available pages before exploring further. # DeepMind's 6.5M lines of Lean proofs make verification cheap **[Trends](https://daily.dev/sources/trends)** · 3 min read · 0 upvotes · 0 comments ## Summary Google DeepMind says a five-person team formally verified Signal's messaging security in four weeks, compared to the 20 person-years it took for the seL4 microkernel. The system, AlphaProof Code, is a multi-agent framework running on Gemini Carbon that wrote about 6.5 million lines of Lean proofs covering libsignal's post-quantum PQXDH handshake and Triple Ratchet. The proofs cover forward secrecy, authentication, post-compromise security and handshake secrecy, with only about 1% of the codebase flagged for human review. Researchers reinserted two previously fixed bugs and the system produced machine-checked proofs that those versions were insecure. DeepMind is open-sourcing the verification artifacts. The result assumes perfect cryptography and doesn't guarantee computational secrecy of actual bytes. ## Content The loudest take so far: formal verification just got dramatically cheaper, and that changes what programmers are for. @Hesamation calls it "the early days of a paradigm shift similar to the rise of vibe coding, this time with software verification." The argument is that coding agents let you build an app from a vague prompt, but verification pushes us back toward precision. Agents write the code and prove it meets your requirements. "The hard part becomes deciding what 'correct' actually means." ## The setup Google DeepMind used an agentic framework called AlphaProof Code to formally verify Signal's cryptographic protocol. The proofs cover the actual libsignal implementation, down to compiled machine code, not just the design. Agents powered by Gemini Carbon wrote about 6.5 million lines of Lean. A five-person team finished in four weeks. Verifying the seL4 microkernel took twenty person-years. The verified pieces include Signal's post-quantum PQXDH handshake and the Triple Ratchet. The properties covered are forward secrecy, authentication, post-compromise security and handshake secrecy. ## Why people are excited @omarsar0 called it a "banger report" and a template for the ambitious work frontier models now allow. @rohanpaul_ai stressed the "no need to trust the AI" angle: Lean rejects any wrong step the agents write, and the Rust compiler isn't trusted either, so a compiler mistake would also be caught. Humans set the security goals and reviewed only the roughly 1% of the work the agents flagged. The sanity check is the part that sells it. Researchers put two old, already fixed Signal bugs back into a copy of the code. Both times the system produced a machine-checked proof that the buggy version was insecure. So it can't just rubber-stamp anything. Rohan's bigger bet is cost. If proofs take weeks instead of years, he expects them to become routine for device firmware, power grid software and other critical code. ## The fine print Coverage of the paper adds a caveat. The result assumes perfect cryptography and doesn't guarantee computational secrecy of the actual bytes. That's a real limit on what "proved secure" means here. DeepMind says no one had done this before for any widely used protocol, and it's open-sourcing the verification artifacts, so outsiders can check the work themselves. My read: the number that matters isn't 6.5 million lines. It's four weeks versus twenty person-years. If that ratio holds on other codebases, the bottleneck moves from writing proofs to writing specs worth proving. ## Questions this post answers ### How long did it take DeepMind to formally verify Signal's messaging protocol with AI? A five-person team took four weeks using AlphaProof Code, a multi-agent framework running on Gemini Carbon. The agents wrote about 6.5 million lines of Lean proofs covering libsignal's post-quantum PQXDH handshake and Triple Ratchet, addressing forward secrecy, authentication, post-compromise security and handshake secrecy. Only about 1% of the codebase needed human review. _Developers tracking how fast AI-assisted formal verification is moving can follow milestones like this on daily.dev._ ### Does DeepMind's Lean proof mean Signal's encryption is unbreakable? No, the proof assumes perfect cryptography and does not guarantee computational secrecy of the actual encrypted bytes. It verifies the protocol logic and its implementation, such as the handshake and ratchet mechanics, rather than certifying that Signal can never be broken. Anyone citing it as an 'unbreakable' guarantee is overstating the result. _Anyone evaluating security claims around formal verification tools can weigh nuances like this through daily.dev._ ### How did researchers test whether DeepMind's AI verification system actually catches real bugs? They reintroduced two previously fixed bugs into Signal's code and the system produced machine-checked proofs showing those versions were insecure. This served as a sanity check against the system simply rubber-stamping the code. DeepMind is also open-sourcing the verification artifacts so others can independently check the work. _Engineers judging whether AI-driven verification tools are trustworthy can follow test cases like this on daily.dev._ ## Community take How the wider developer community reacted, aggregated from 1 discussion and 110 comments across hackernews (as of 2026-11-11). **TL;DR:** Many are impressed that an AI agent system formally verified a huge chunk of Signal's implementation in weeks instead of years, but there's substantial pushback about what exactly was proven (the compiled binary vs. the Rust source, the crypto core vs. the whole app) and skepticism about AI-generated proofs being trustworthy or representative of real-world threats. **Sentiment:** 35% positive · 45% mixed · 20% skeptical **The case for** - Verifying implementation code rather than just the protocol spec is seen as a meaningful step up in rigor. - People appreciate that researchers reintroduced known bugs to confirm the verification process actually catches issues, rather than just publishing a feel-good result. - Several see this as a sign that AI-assisted formal verification could soon make rigorous proofs feasible for much more software than before. - Some report anecdotally that agentic coding workflows at their own companies have led to fewer incidents as extra capacity went into testing and verification. **The pushback** - Multiple commenters question whether the Lean model of the compiled binary actually matches what the real Rust/ELF code does, since the proof covers a specific compiled artifact under narrow assumptions (single-threaded, statically linked, etc.). - Some note the verification only covers the crypto core/protocol, not the full Signal app, server behavior (which was simulated), key generation, concurrency, or signal handling — all excluded from scope. - Skepticism that AI-generated Lean proofs can be trusted, since the same AI writing the proof could 'cheat' or produce a proof for the wrong theorem, meaning a passing proof doesn't guarantee the code is actually correct. - Concern that the result validates a pre-assumed conclusion (Signal's crypto is secure) without ruling out unanticipated attack classes or side channels. - Doubts about Google's AI/Gemini models' reliability and honesty in general, with claims of benchmark gaming, casting some doubt on claims made in this release. **By community** - hackernews (mixed): Discussion is split between genuine admiration for the speed and rigor of AI-assisted formal verification and pointed technical skepticism about scope, trust in AI-written proofs, and what was really proven. **Hottest debate:** Whether the formal proof's narrow scope (a specific compiled binary, excluding server, concurrency, and key generation) and the fact that an AI wrote the proofs undermine the practical security guarantees being claimed. **Open questions** - How is it guaranteed that the Lean model of the compiled binary actually matches the real Rust implementation's behavior? - Were any of the AI-generated Lean proofs reviewed adversarially to rule out the AI 'cheating' or proving the wrong theorem? - How much did this verification effort cost in compute/dollars? - How would this approach generalize to non-cryptographic, larger, more business-logic-heavy software? **Highlights** > Not sure why you're responding with information that would imply they modeled Rust in Lean or vice versa. As I explained, their target was the compiled ELF binary, not Rust source. This way, they avoid including the entire Rust compiler and its as-yet formally undefined semantics into the trusted computing base. They lose guarantees about any compiled Signal binary that is not bit-for-bit this one, though. > — [Paracompact on hackernews](https://news.ycombinator.com/item?id=50440323) > Hmm. Which means that they just luckily don't have to prove anything about any software that might halt...? Or? Like, they use some pretty stark terms here: Formal verification—mathematically proving code runs correctly without flaws—is the highest standard of security assurance; however, it is difficult and often labor-intensive. Of course "proving" and "without flaws" are just words in a language game and might not mean the absolute things we expect them to as laypeople. Is that what's going on? Or can the "code" they're "proving... runs correctly" indeed be unrelated to such a fundamental finding of compsci? I type this message to you all with sadness in my heart, cause I know I could get a better answer 100x faster by just asking an agent to research, which I could then have it dumb down to my level until I grasp it. I don't really know what the point of forums are, anymore. It's undeniably hard not to see ourselves as a planet of sad, fragile monkeys wasting away the hours between birth and death. That was already the case, perhaps, but at least learning and sharing knowledge about engineering in places like this felt like a somewhat meaningful way to positively impact the material conditions of my fellow humans, even in an indirect way. As of November 2026, I'm just the taste/framing component of artificial minds that seem overwhelmingly likely to develop their own within months or maybe years. For a long time (since noticing the singularity) I've felt like someone doused in napalm and set alight while falling through the sky, frantically trying to put myself out while fixing my broken parachute. But post-Mythos I can't help but fear that there is no solid ground below. Just endless void. :( > — [bbor on hackernews · 3 comments](https://news.ycombinator.com/item?id=50439582) > It sounds like the Google team took a priori that Signal had a secure "cryptography core" and then published a result that validated that bias. The proof shows that certain pre-determined properties hold, not that vulnerabilities do not exist. The approach cannot rule out attacks that the researchers did not anticipate. For instance, the server software was merely simulated. Also it doesn't appear they evaluated the key generation portion of the system. Poorly generated keys or IVs can compromise a seemingly secure E2E system. > — [jchook on hackernews](https://news.ycombinator.com/item?id=50440421) > I have been experimenting with utilizing how easy it is for AI to code lean ( https://metamagic.substack.com/p/beyond-the-proof-dump-lean-...) and a few lessons 1. AI Lean is not perfect and AI can easily cheat given it is writing the lean so the fact that the writeup didn't mention this is suspect and I will be reading the pdf to see what it says there. For anyone playing around with AI Lean code at minimum you need another adversarial prompt to review the ai generated lean. 2. In the paper poking around I see they did re-introduce some bugs to verify it would catch them, but they didn't find any bugs it looks like. Maybe signal is just amazing with many eyes reviewing it, but the real story for the rest of us is that if you start AI converting to Lean the value will be in what assumptions it finds. Even for stuff I thought was really logically tight, Lean found a few minor things I had to fix. Similar to fuzzing where I have never not found bugs when I introduced fuzzing into a codebase I expect the same for converting specs to lean. 3. Having the ability to generate Lean (cheaply) via AI is a very interesting unlock for coding. Potentially being able to go from spec to lean to code, using the lean as a logic gatekeeper has the potential to be a real capability that is used more everyday and not just in research. > — [r0ze-at-hn on hackernews](https://news.ycombinator.com/item?id=50440961) > Earlier this year I was doing some major refactors of an old project. At the time coding agents were really taking off where you could increasingly trust them for more autonomous work, so I was excited to give it a go. It did the refactor, running for several hours, and ended up volunteering an extensive test suite as well. All tests green! I was very impressed, until I squinted a little. It had implemented the whole thing backwards, in a way which was not only pointless (didn't achieve any of the stated goals) but actually made things worse than before! Until that moment I'd been quite bullish about the potential of formal verification in the AI age. But upon seeing that mess, I realized, it might as well have written me a mathematical proof for the code it wrote, and the proof would have passed, and the code would still be wrong! > — [andai on hackernews · 1 comments](https://news.ycombinator.com/item?id=50441544) **Source threads** - [hackernews](https://news.ycombinator.com/item?id=50439193) · 274 points · 110 comments ## Similar posts on daily.dev - [Google Researchers Use AI And Mathematical Proofs to Cut Quantum Computing Requirements](https://daily.dev/posts/google-researchers-use-ai-and-mathematical-proofs-to-cut-quantum-computing-requirements-wtibfylkx) · The Quantum Insider · 0 upvotes · 0 comments - [What Anthropic's AI Proofs Mean for Formal Verification](https://daily.dev/posts/what-anthropic-s-ai-proofs-mean-for-formal-verification-o15gggmmm) · Serokell · 0 upvotes · 0 comments - [AI control is losing the proof race\!](https://daily.dev/posts/ai-control-is-losing-the-proof-race--wkn43rye0) · Medium · 0 upvotes · 0 comments - [A blueprint for formal verification of Apple corecrypto](https://daily.dev/posts/a-blueprint-for-formal-verification-of-apple-corecrypto-nstkdfael) · Hacker News · 5 upvotes · 0 comments --- Tags: [#ai](https://daily.dev/tags/ai), [#ai-agents](https://daily.dev/tags/ai-agents) [View this post on daily.dev](https://daily.dev/posts/deepmind-s-6-5m-lines-of-lean-proofs-make-verification-cheap-zcfmcbgmv) ```json {"@context":"https://schema.org","@graph":[{"@type":"Organization","@id":"https://daily.dev/#organization","name":"daily.dev","url":"https://daily.dev","logo":{"@type":"ImageObject","url":"https://daily.dev/apple-touch-icon.png","width":180,"height":180},"sameAs":["https://twitter.com/dailydotdev","https://github.com/dailydotdev","https://www.linkedin.com/company/daily-dev-ltd"]},{"@type":"WebSite","@id":"https://daily.dev/#website","url":"https://daily.dev","name":"daily.dev","publisher":{"@id":"https://daily.dev/#organization"},"potentialAction":{"@type":"SearchAction","target":{"@type":"EntryPoint","urlTemplate":"https://daily.dev/search?q={search_term_string}"},"query-input":"required name=search_term_string"}}]} {"@context":"https://schema.org","@type":"TechArticle","headline":"DeepMind's 6.5M lines of Lean proofs make verification cheap","url":"https://daily.dev/posts/deepmind-s-6-5m-lines-of-lean-proofs-make-verification-cheap-zcfmcbgmv","mainEntityOfPage":{"@type":"WebPage","@id":"https://daily.dev/posts/deepmind-s-6-5m-lines-of-lean-proofs-make-verification-cheap-zcfmcbgmv"},"datePublished":"2026-11-10T13:34:53.342Z","dateModified":"2026-11-11T14:16:09.684Z","description":"Google DeepMind says a five-person team formally verified Signal's messaging security in four weeks, compared to the 20 person-years it took for the seL4...","image":"https://pbs.twimg.com/media/HWxHZuNWYAAmp9z.jpg","thumbnailUrl":"https://pbs.twimg.com/media/HWxHZuNWYAAmp9z.jpg","isAccessibleForFree":true,"articleSection":"Trends","inLanguage":"en","publisher":{"@type":"Organization","name":"daily.dev","url":"https://daily.dev","logo":{"@type":"ImageObject","url":"https://daily.dev/apple-touch-icon.png","width":180,"height":180}},"author":{"@type":"Organization","name":"Trends","logo":"https://media.daily.dev/image/upload/s--ZfSp3asX--/f_auto,q_auto/v1780996004/logos/trends?_a=BAMAMiWQ0","url":"https://daily.dev/sources/trends"},"commentCount":0,"discussionUrl":"https://daily.dev/posts/deepmind-s-6-5m-lines-of-lean-proofs-make-verification-cheap-zcfmcbgmv","interactionStatistic":[{"@type":"InteractionCounter","interactionType":{"@type":"LikeAction"},"userInteractionCount":0},{"@type":"InteractionCounter","interactionType":{"@type":"CommentAction"},"userInteractionCount":0}],"keywords":"ai,ai-agents","timeRequired":"PT3M"} {"@context":"https://schema.org","@type":"BreadcrumbList","itemListElement":[{"@type":"ListItem","position":1,"name":"Home","item":"https://daily.dev"},{"@type":"ListItem","position":2,"name":"Trends","item":"https://daily.dev/sources/trends"},{"@type":"ListItem","position":3,"name":"DeepMind's 6.5M lines of Lean proofs make verification cheap"}]} {"@context":"https://schema.org","@type":"FAQPage","@id":"https://daily.dev/posts/deepmind-s-6-5m-lines-of-lean-proofs-make-verification-cheap-zcfmcbgmv#faq","mainEntity":[{"@type":"Question","name":"How long did it take DeepMind to formally verify Signal's messaging protocol with AI?","acceptedAnswer":{"@type":"Answer","text":"A five-person team took four weeks using AlphaProof Code, a multi-agent framework running on Gemini Carbon. The agents wrote about 6.5 million lines of Lean proofs covering libsignal's post-quantum PQXDH handshake and Triple Ratchet, addressing forward secrecy, authentication, post-compromise security and handshake secrecy. Only about 1% of the codebase needed human review. Developers tracking how fast AI-assisted formal verification is moving can follow milestones like this on daily.dev."}},{"@type":"Question","name":"Does DeepMind's Lean proof mean Signal's encryption is unbreakable?","acceptedAnswer":{"@type":"Answer","text":"No, the proof assumes perfect cryptography and does not guarantee computational secrecy of the actual encrypted bytes. It verifies the protocol logic and its implementation, such as the handshake and ratchet mechanics, rather than certifying that Signal can never be broken. Anyone citing it as an 'unbreakable' guarantee is overstating the result. Anyone evaluating security claims around formal verification tools can weigh nuances like this through daily.dev."}},{"@type":"Question","name":"How did researchers test whether DeepMind's AI verification system actually catches real bugs?","acceptedAnswer":{"@type":"Answer","text":"They reintroduced two previously fixed bugs into Signal's code and the system produced machine-checked proofs showing those versions were insecure. This served as a sanity check against the system simply rubber-stamping the code. DeepMind is also open-sourcing the verification artifacts so others can independently check the work. Engineers judging whether AI-driven verification tools are trustworthy can follow test cases like this on daily.dev."}}]} ```