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.

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.

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.

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...

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.

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.

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)?

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.

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.