AlphaProof Code

Computer0

I'm pleased to read Signal looks good to our robot mindlords.

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.

yread

They thank Sundar Pichai. I guess it makes sense but at the same time...

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

xrisk

wonder how many dollars were spent on this

nurumaik

Now pls do telegram to settle "telegram shouldn't have invented their own crypto" debate once and for all

fercircularbuf

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.

hmokiguess

From the paper: https://google-deepmind.github.io/code-verification/

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.

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.

whattheheckheck

How do you prove the lean code represents what the code its proving?

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?

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.

beernet

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

hoppp

This is the way. I have been working on similar. Since code is cheap there is no excuse to not have verification everywhere.

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.

0o777

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.

nicou

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

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.

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.