Something seems wrong here. They took a non-trivial piece of human-written code that has had bugs in the past, formally verified the whole library, and found zero bugs?
I can believe that it's possible to get the LLM to write proofs, but I can't believe there were zero bugs in the system they verified. I wonder if they got the theorems wrong, or if they only proved narrow properties of the system.
I've had Claude formally verify crypto and data storage formats. It wrote theorems that looked fine and the formal verification passed but the resulting code contained many, many bugs that other implementations of the same things found with ad hoc testing.
The way the announcement is written, we should expect zero bugs in libsignal moving forward, and I guess time will tell whether that happens or not.
show comments
thibsrn
Great, what a great use case for AI. I feel like Google has been the cleanest of the big players in terms of useful contributions and control of their AI systems. This new proof agent doesn't seem to challenge the spec though, just the implementation, if I've understood correctly.
I wonder how this agent is different than a classic coding agent, in the end it seems to work the same way, iterating over a codebase while writing Lean or Rocq code and running it.
show comments
andai
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!
show comments
Mizza
I'm expecting that very soon, perhaps in the next two or three years, it will seem mad that we ever ran _any_ unverified software on our systems, like how it now seems mad we used Telnet or plaintext HTTP.
show comments
joss82
The problem with verifying real-world software is to give a clear and unambiguous definition of what "correct" means in context.
You cannot catch bugs in the specs that way.
ghm2180
Noob Question: Apart from these cryptographic systems would it be useful to build these proofs for general pieces of software? Specifically:
1. Has someone applied it to software systems where an AI agent is in the critical path in production i.e. non-deterministic action may occur(albeit with recovery)?
2. What scenarios does it make sense to have a lean proof from the start? Like i imagine if you wanted to make a database system with some guarantees around ACID then it might be better having this from the get go. But probably not that useful for building an API backed service.
1. AI Lean is not perfect and AI can easily cheat given it is writing the lean. 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.
Awesome. I remember thinking last year that software is about to get a lot more buggy now that people are offloading more to AI, but tools like this give me hope that perhaps the future of software actually looks a lot more safe.
Software verification with AI feels powerful.
We built a way to find bugs by building simple formal proofs of risky functions and it routinely finds racing conditions and other harder to spot bugs.
How trusted are Intel's (SGX) and AMD's hardware level security features?
Cloudflare runs their edge network in random ISP datacenters and in shady jurisdictions and promise AMD's TSME is enough to keep things secure.
show comments
ctrlaltdileep
This is pretty cool. I appreciate that they reintroduced security bugs into the implementation to confirm that their process was actually catching issues. I feel like so many "look what AI did!" articles these days focus on the fact that AI did something and not about whether it did it correctly or not. Nevertheless I hope we will get more reliable libraries and dependencies out of this.
sim04ful
Curious question, in this case for verification they ported the software into a formal mathematical model. Why can't software development start from the other end instead ? Start with a formal model with the properties you want, then translate it into software.
show comments
fefaOd
Saving man-hours is a big deal. Progress opens more and more doors, the main thing is not to open the last one.
>> AlphaProof Code is a multi-LLM agentic framework that splits the work of formal verification the way a research team would
Not sure if this is precise. At least it sounds somewhat odd. I think what they really wanted to say here is "multi-agent system" (which usually, but not necessarily, implies the use of multiple LLMs).
pvab3
Isn't this kind of a major blow to human software developers? Now code can be generated and tested independently of human expertise, both much faster than a human could.
show comments
whattheheckheck
How do you prove the lean code represents what the code its proving?
throwaway198846
I hope it will be possible to verify CPUs soon as well. Of course that is much harder because they are not open source and physical and you need to simulate physics to verify them fully.
show comments
hoppp
This is the way. I have been working on similar.
Since code is cheap there is no excuse to not have verification everywhere.
xrisk
wonder how many dollars were spent on this
show comments
yread
They thank Sundar Pichai. I guess it makes sense but at the same time...
show comments
dinogo
I feel that paradigms like this, is going to be the standard going forward.
m3kw9
Just input the link to your llm and ask it how it applies to you
paganel
I'm not at all versed in this "formal proofing" thing, but without diving all that much into it how does this handle the halting problem (and the related problems that in the end all point to said halting problem)?
show comments
nimitbhardwaj
Nice
nurumaik
Now pls do telegram to settle "telegram shouldn't have invented their own crypto" debate once and for all
show comments
whattheheckheck
"human experts work with AI to decide what to prove"
Why can't ai do this too? Is this the fundamental limit of ai?
show comments
p-e-w
It’s nothing short of amazing that a huge codebase like Signal’s is apparently not only secure in a practical sense, but secure even in a strict formal sense. The people who wrote the Signal code must be engineers of the highest caliber.
show comments
Computer0
I'm pleased to read Signal looks good to our robot mindlords.
dmead
did the formal proofs for the haskell compiler stop bugs from happening?
Something seems wrong here. They took a non-trivial piece of human-written code that has had bugs in the past, formally verified the whole library, and found zero bugs?
I can believe that it's possible to get the LLM to write proofs, but I can't believe there were zero bugs in the system they verified. I wonder if they got the theorems wrong, or if they only proved narrow properties of the system.
I've had Claude formally verify crypto and data storage formats. It wrote theorems that looked fine and the formal verification passed but the resulting code contained many, many bugs that other implementations of the same things found with ad hoc testing.
The way the announcement is written, we should expect zero bugs in libsignal moving forward, and I guess time will tell whether that happens or not.
Great, what a great use case for AI. I feel like Google has been the cleanest of the big players in terms of useful contributions and control of their AI systems. This new proof agent doesn't seem to challenge the spec though, just the implementation, if I've understood correctly.
I wonder how this agent is different than a classic coding agent, in the end it seems to work the same way, iterating over a codebase while writing Lean or Rocq code and running it.
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!
I'm expecting that very soon, perhaps in the next two or three years, it will seem mad that we ever ran _any_ unverified software on our systems, like how it now seems mad we used Telnet or plaintext HTTP.
The problem with verifying real-world software is to give a clear and unambiguous definition of what "correct" means in context.
You cannot catch bugs in the specs that way.
Noob Question: Apart from these cryptographic systems would it be useful to build these proofs for general pieces of software? Specifically:
1. Has someone applied it to software systems where an AI agent is in the critical path in production i.e. non-deterministic action may occur(albeit with recovery)?
2. What scenarios does it make sense to have a lean proof from the start? Like i imagine if you wanted to make a database system with some guarantees around ACID then it might be better having this from the get go. But probably not that useful for building an API backed service.
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. 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.
I'm curious how their approach compares with what Theorem & Anthropic are trying to do with formally proving nixpkgs: https://theorem.dev/blog/verified-software-stack/
Awesome. I remember thinking last year that software is about to get a lot more buggy now that people are offloading more to AI, but tools like this give me hope that perhaps the future of software actually looks a lot more safe.
Nice to see this actually being done. I thought it was a very interesting idea when I read Martin Kleppmann's post about it a while back: https://martin.kleppmann.com/2025/12/08/ai-formal-verificati...
Software verification with AI feels powerful. We built a way to find bugs by building simple formal proofs of risky functions and it routinely finds racing conditions and other harder to spot bugs.
https://verity.md/benchmark#calcom
Do I understand correctly that they verified the entire libsignal Rust library and not just a human-written spec of the Signal protocol?
Also I noticed something in the libsignal repo:
>attest: Functionality for remote attestation of SGX enclaves and server-side HSMs
https://github.com/signalapp/libsignal
How trusted are Intel's (SGX) and AMD's hardware level security features?
Cloudflare runs their edge network in random ISP datacenters and in shady jurisdictions and promise AMD's TSME is enough to keep things secure.
This is pretty cool. I appreciate that they reintroduced security bugs into the implementation to confirm that their process was actually catching issues. I feel like so many "look what AI did!" articles these days focus on the fact that AI did something and not about whether it did it correctly or not. Nevertheless I hope we will get more reliable libraries and dependencies out of this.
Curious question, in this case for verification they ported the software into a formal mathematical model. Why can't software development start from the other end instead ? Start with a formal model with the properties you want, then translate it into software.
Saving man-hours is a big deal. Progress opens more and more doors, the main thing is not to open the last one.
From the paper: https://google-deepmind.github.io/code-verification/
>> AlphaProof Code is a multi-LLM agentic framework that splits the work of formal verification the way a research team would
Not sure if this is precise. At least it sounds somewhat odd. I think what they really wanted to say here is "multi-agent system" (which usually, but not necessarily, implies the use of multiple LLMs).
Isn't this kind of a major blow to human software developers? Now code can be generated and tested independently of human expertise, both much faster than a human could.
How do you prove the lean code represents what the code its proving?
I hope it will be possible to verify CPUs soon as well. Of course that is much harder because they are not open source and physical and you need to simulate physics to verify them fully.
This is the way. I have been working on similar.
Since code is cheap there is no excuse to not have verification everywhere.
wonder how many dollars were spent on this
They thank Sundar Pichai. I guess it makes sense but at the same time...
I feel that paradigms like this, is going to be the standard going forward.
Just input the link to your llm and ask it how it applies to you
I'm not at all versed in this "formal proofing" thing, but without diving all that much into it how does this handle the halting problem (and the related problems that in the end all point to said halting problem)?
Nice
Now pls do telegram to settle "telegram shouldn't have invented their own crypto" debate once and for all
"human experts work with AI to decide what to prove"
Why can't ai do this too? Is this the fundamental limit of ai?
It’s nothing short of amazing that a huge codebase like Signal’s is apparently not only secure in a practical sense, but secure even in a strict formal sense. The people who wrote the Signal code must be engineers of the highest caliber.
I'm pleased to read Signal looks good to our robot mindlords.
did the formal proofs for the haskell compiler stop bugs from happening?
holy shit