AlphaProof Code
deepmind.google
deepmind.google
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.
It's that, yes.
They didn't prove that the code has no bugs; they proved that none of the current bugs (known or unknown) are security-breaking bugs, per their formalized security model.
> First, our researchers collaborated with a mix of models to translate Signal’s security goals into formal mathematical specifications, with human experts reviewing every one. From there, agents powered by Gemini Carbon did the proofs, generating over six million lines of Lean, a computer language that mathematically proves the accuracy of code.
The generated Lean code here is just being checked against the "formal mathematical specifications of Signal's security goals", not checked for the low-level properties you might care about as a programmer, e.g. "will it ever leak memory" or "will it ever crash", etc. And in fact, the code is not even being checked for the reachability of non-security-violating protocol failure states, e.g. "could the protocol ever deadlock such that neither side can send messages any more".
It's still perfectly possible for the code to have all of these problems. It's now just known that, as of the commit they did this analysis against, none of those low-level problems, as far as they exist in the codebase, can cause a security-model violation.
Or, to put that another way: the system has been proven to "fail safe" in all its current failure modes, per their specific definition of safety (which is basically "keeping to the security guarantees Signal markets itself to users as having".)
They took signals security goals/aim/target and used models to generate a mathematical model. Which is a bit “hey trust us bro” in 3 ways but they did have human experts fully review 1 path, partially review 1 path, and the last I’m not really sure.
The fully reviewed path was that the aims goals were turned into positive mathematical statements “we will achieve X Y Z” so if we trust the humans that part should be as strong as we achieved X Y Z.
Tons of lean code generated to prove X Y Z correct, a lot of it is entirely self consistent. But then because it’s too much to look at we had the AI judge all of it for problem areas and we had humans look at that 1% of it… okay? That’s great if your magic box can pick out the problem areas but that wasn’t proved.
My last issue is, and please tell me if I’m wrong or missed something, but what says or proves the security goals/models are necessary and sufficient? We aim to do X Y Z. Great. We aim to not do A B C. not sure if I’m quibbling or this is strictly needed but it seems missing (unless it can be captured in entirely in the positive statement) let’s assume it’s included. We did X Y and Z, we did not do A B or C. Okay what’s my prize? Unbreakable crypto?
“Um well no… we know we can have X Y and Z while not having A B and C”
And so if we have X Y Z none of A B C we know the model is good.
“Yeah, probably”
And that the code at some point in time is no better than that?
“Yeah, certainly”
Proofing and securing those is the way larger attack vector and work to come.
I had assumed them to mean the latter, since I don't think the protocol design specification on its own would shake out into "over six million lines of Lean code." (Though if someone who knows Lean well thinks that's actually a reasonable number, please do correct me.) 6MM lines of proof code sounds more like something you get by "translating" an average-sized self-contained imperative-language library (like the protocol impl library) into a highly-rigorous prover language line-by-line, with a lot of the overhead coming from having to model imperative-language / imperative-CPU-target-abstract-machine semantics in rigorous mathematical form.
Annoyingly, the wording of the article is a bit too ambiguous to say for sure either way. They just say they "generated" the Lean code; they didn't say what it was being generated from.
Also, I presume there are some unproved baked in assumptions about cryptographic primitives (e.g, but not necessarily, "sha512 has a uniform distribution")
Software doesn't exist in a platonic state like formal mathematics, which at least can be consistent with all other results. Software interacts with the real world and "bugs" can be any number of security weaknesses like emitting useful timing signatures, buffer overflows that depend on the compiler used, weaknesses on certain hardware, etc.
It is great that Google has formalized code to some degree and for software that MUST be hardened, this may be valuable. It may be generally useful, but we need to get a feel for the gaps that inevitably will persist.
Doesn't it? Like all these things you can model in the end, your state space, and thus necessary proofs and even just the spec itself would explode in size.
But that's how every single model works.
Real software needs mind blowingly complex specifications and while it's now fairly easy to get an AI generated proof that your code follows the spec, there's not much to help you with bugs in the spec.
AI will happily change the spec for you so the code verifies though, but that doesn't solve the trust issue.
Truly a trusting trust scenario.
But even then, what's not possible is to "know" whether the spec=code is whatever the creator actually had in mind.
But still, the target programming language's formalism is still likely done on a higher level, than e.g. its compiler output on a given CPU, so compiler bugs could still "throw a wrench" into the system.
So this wouldn't prove as much as you think. Especially since both tge experts and the LLMs behind this are well aware of Hearbleed - so them finding Hearbleed wouldn't tell you anything, really.
Well, if it's SSH then I sure hope it has no LLM-discoverable bugs.
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.
Or you can use verus instead which does automatic mapping from the rust code to the proof where possible.
Aggressively staggeringly high rates of straight up making shit up and covering up the lies. Gemini 3.5 flash was comical because it would delusionally scream nonsense like "we're go-go ready!!! :tada:" while the code didn't compile (I swear the only reason people thought that was a good model was because they didn't use it) and their models just got better at making tool calls without fixing it's tendency to cheat.
Gemini models are not looking all that good here: https://maxxbench.unlap.ai/
They got a lot of shit for it at the argon launch and you'll notice the carbon release blog has a lot of detail on how they focused on misalignme t and fabrication rates: https://blog.google/innovation-and-ai/models-and-research/ge...
So Google themselves is not behaving like they think people are making stuff up about their models behavior.
Google itself is also just behaving in such a sleazy way. "Carbon is the best model ever but also you can't use it yet." Watch them release it now that fable is out and nobody cares anymore so nobody checks to see how much they benchmaxed lol. They're clearly under some sort of internal pressure to pretend they're at the frontier and that's bleeding through I to the frenetic pace of model releases they've had in the past couple months through Argon and Carbon. Bleeding through in the sense of the models also only really care about benchmarks and good news cycles. Again they did claim they tried to solve a lot of this for carbon but they didn't let people use the model and once you have a base model that cheats benchmarks you have to wonder if it actually lies less or just gets caught less, but hopefully they got things back on track?
Fucking called it: https://blog.google/innovation-and-ai/models-and-research/ge...
They've been releasing their models 2 weeks after the first announcement. I doubt Google is timing their GA against Anthropic unless they had knowledge of when exactly Anthropic was releasing theirs.
Also, I've been using Carbon vs Opus 5.5 and Carbon is a great model. Haven't seen any hallucinations. Argon was well known to be a worst programming model than Opus via benchmarks, so you and influencers broadcasting a well kept secret.
Compared to the other LLMs I've used, it seems to have system instructions that are far more adversarial to the user.
They all don't trust each other.
It's going to take way more than throwing a more advanced LLM at the problem to make any progress.
You (they) cannot even prove Collatz, how are you planning to prove Powerpoint?
1. Because everything everywhere is getting hacked
2. For the same reasons people are already decomping games and rebuilding Photoshop and stuff - because they can and don't want to pay for proprietary options.
3. Because of the exact same dynamics of fast fashion? I'm not sure how fast fashion supports your point. Fast fashion is specifically not maintaining old clothes and treating all clothes as disposable slop and rotating through them. That dynamic in software is all software becomes single use throwaway and formalization as a part of the agent loop based on some set of standards is a pretty good way to make that tractable
What is more likely, for AI agent that is trained with the goal of making user believe their problem is solved to solve exceedingly hard problem by developing novel theory, or to come up with plausible looking fake solution to the problem?
Fast fashion was mentioned as parallel to fast software — no incentives to lose profits.
BB is proving things about all turning machines of a general size and it's unsolvable in general because 1. above a certain size you're encoding all the unsolved problems of mathematics 2. Halting problem.
BB and halting problem is also totally irrelevant here. We're talking about proving specific things about specific pieces of software, where we can change the software implementation to make the desired invariants easier to prove. Obviously there's the well known catch of just because you proved x doesn't mean that x being true implies whatever y behavior (security, class of bugs, etc) you're actually interested in but like, that's why we have standards committees and stuff. And the nice thing is there's sort of an evolutionary pressure when it comes to figuring out the right invariants for security in that anything you do will get aggressively stress tested by swarms of increasingly capable agents.
In terms of the alignment problem - the latter is possible and a risk but also you're talking about reward hacking like it's some gotcha instead of a thing people have been thinking about for decades and are spending hundreds billions of dollars on given at least the national security needs here and at worst the risk of catastrophic misalignment/rogue swarms. The huggingface hack is fresh in everyone's memory
No plans on that front. Instead, I write my software from the start using a methodology of formal specification and proof. And at some point (1 year from now?) that software will include something much better and cooler than Powerpoint.
However yes, anything formal can help and if AIs can hide it from ourselves (we won't be able to follow it) and make it their internal design language chances are that it's going to be really used.
What if we could do that to popular web frameworks?
And than, what if we had tools that could easily define, specific security properties of web sites built on these platforms? For example, "no data ever flows between different users, unless it's via specific API call by the user's code?"
And if we can define a security property, in a specific application, for ex. slack that says "data in a chat between two group members can only go to the group manager, if the setting "manager as god" is set by both users", and the AI can formally verify that? And than have a short file defining all the security properties we want for out specific application ?
And than have AI formally verify all of that?
The biggest hurdle is probably the number of bugs in most code. Verification would mean fixing all of those as well.
> Apple A series processors beginning with the A7 contain a Secure Enclave coprocessor running an L4 operating system called sepOS (Secure Enclave Processor OS) based on the L4-embedded kernel developed at NICTA in 2006.
Are you sure that sepOS was formally verified? seL4, also from NICTA, was formally verified, but I don't think L4-embedded or sepOS were.
I think this is an incredible result and I hope we'll see more and more of it, but even still, it's verifying a pretty thin slice of an actually executing system!
Verification isn't a panacea though. The hard lesson everyone learns when they first start taking an interest in verification is that perfect verification is fundamentally impossible.
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!
Now, write a theorem describing a non-trivial piece of software. Is your theorem longer or shorter than the source code? Easier or harder to read?
Say, no crashes, no dead or livelocks, O(n log n) in the size of the input, same number of instructions executed & memory accessed no matter what the encryption key is, etc etc.
These type of theorems are significantly smaller than the source code, pretty re-usable across different applications, and extremely useful properties.
Obviously you don't write "a theorem" describing a big piece, but just a fuinction, for example.
Say you have a function that takes in 3 Points (x,y coords) and returns a Triangle (T) object. Than you can have a property test that will confirm that T is actually a triangle and not something else.
And then you need to remind that it does not matter, if they are empty.
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.
My current workflow is i have a coordinating agent, and then a bunch of long running sessions that are specialized (CS theory, Kernel, Surface, Lowering/Backend, Corpus, Docs, etc). I only talk to the coordinator, they only accept tasks from the coordinator, but they can ask each other questions. None of them do their own coding, they assign coding tasks to agents/workflows. The main purpose of that is to stop it from blowing out context windows. Each has a million tokens of long term context and their own memory/claude.md etc, and they don't waste it by writing code directly. All work is assigned via github issues and answered with PRs. The coordinator mostly just keeps big picture goals in mind and manages PRs, etc..
I've currently got a fully formally verified borrow calculus and effect algebra, with a formally verified guarantee of memory safety and that all programs either continue (don't get wedged, no deadlocks), or they terminate with the heap empty. The only thing _not_ formally verified is the lowering to LLVM.
The language is mature to the point that I have real programs in it...
The extra velocity has meant we move considerably faster than the product team, so a lot of that extra dev capacity has been channeled into improving our tests, verifications and automated review processes - so hardly anything is slipping through the gaps.
This is the opposite of what I expected when we started working this way. One of the concerns we as a team raised was that it would lead to more bugs and lower quality but after 6 months the opposite appears to be true
Interesting that they end up with 26k lines of specifications (including Arm semantics). That's quite a large trusted computing base. I guess they need to develop the symbolic/computational models from the ground up. It'll be interesting to see if we can develop reusable libraries of these, a la mathlib, and how the incentives work out there. The AI labs are probably not particularly interested in this, and it's also likely to be thankless work for the researchers. But perhaps if companies doing verification or selling verified products do sprout out, maybe there will have an incentive to share the work and have a standardized TCB. That might, for better or worse, also put a practical end to the "interactive theorem prover wars".
It's also interesting how this will play work for code under development. ChatGPT claims that the day after this was released, libsibnal changed substantially :D Perhaps an intermediate-level, untrusted model in Rust could help (where most of the proof relates the Rust model to the spec, and then a more mechanical proof relates the Rust model to the binary); seL4 did this a long time ago. But I've no idea if this is practical, I haven't heard of anything encoding (full) Rust semantics into an interactive theorem prover... not that it's possible to keep up with the news these days anyway, especially if it's not your full time job. Another question that I don't know the answer to is how full-program optimization changes the picture with that, wonder if someone has any insights there.
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.
At least in domains that are "important" (and perhaps everyone thinks their business/API is important?), I'd want this.
For example - Stripe. If I'm using the stripe API, I want it to be guaranteed to work exactly as documented in all scenarios, given that money is at stake?
Getting the Stripe API written in Lean is a different challenge, of course.
Most software verification is proved "for all possible inputs", e.g. the system maintains some invariant regardless of which sequence of actions is taken. Those inputs could be from a user interacting with the software, or they could be API calls made to our library, etc. There's no reason you couldn't model an AI agent's choices in a similar way: i.e. prove that the desired invariants hold, for all possible sequences of actions the AI component might choose.
That might be straightforward, if the AI agent is constrained to pick from a simple set of domain-specific actions. In contrast, we can't say much about a system involving an AI agent with a full Bash shell.
> What scenarios does it make sense to have a lean proof from the start?
It's usually much easier to verify software that was written and structured with that in mind; rather than trying to reason about some arbitrary blob of code after-the-fact. So, if you do want to prove stuff, it should very much be in there from the start.
Without suggesting that this has no value-- it must be noted that such verification only applies on theoretical hardware and to the specific behavior in scope of the verification. Actual hardware is nondeterministic, and an algorithm can be correct while suffering from a side-channel.
And while possible, good luck validating systems against intentional attacks-- fault injection, power tampering, bus attacks....
It is vital that "formally verified within X scope" does not turn into the leaky abstraction "is secure". Go watch Microsoft's talk on XBox security, and what they had to do to make it as secure as it is (primarily: tightly control hardware, code, and platform). It is not something you throw AI at, and it's not something that you can generalize to the entire computing world.
We need proof systems that are designed to work with our programming languages- working with the code so it more likely represents reality. I like verus with Rust and I have a skill for using it: https://github.com/gregwebs/skills-sdlc/blob/main/skills/rus...
It seems the work of Google involved more experts work, although it might be more about how things are presented. Also this work on Signal contains a substantial specification and verification of the cryptographic protocol, something requiring specialists of the field. On the Anthropic & Theorem side, the specification is more general (and hence lighter): memory safety and absence of assert failures. They target also various software instead of Signal in particular.
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.
Use s real password with the signal account thing.
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).
> The resolution (decompression) of such backreferences in an imperative context is trivial, but uses lots of invariants that make it hard to prove correct. In a purely functional context, it is non-trivial to find data structures that are fast enough. We decided to stick with purely functional algorithms, as they can be verified directly using Coq, and optimization of purely functional programs is interesting for its own sake. In our current verified implementation, this is the slowest part. The benchmarks in Appendix 0.A support this claim. We already have figured out an algorithm with better performance, but we are not yet done proving it formally correct; we will not get deeper into this algorithm in this paper.
There are many ways verify programs; the authors of your linked paper just chose a method that resulted in a slow binary. Alternatively, one can build a model of an imperative language (C) and prove that an imperative programs meets some specification.
You cannot catch bugs in the specs that way.
Since code is cheap there is no excuse to not have verification everywhere.
Cheaper? Faster? More faihtful? Finds more defects in the source software? Unclear.
And just to add, this is also true of "human" mathematics as well.
answer to the first is same as always - by simply not guaranteeing that everything is provable, especially in finite amount of time
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.
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. :(
The difficulty lies in coming up with the right formulations, and also some times altering the program to make it amenable to proof. It's quite often the case that a proof won't go through unless the program itself has the right idea.
As for the halting problem: it is highly theoretical. Lots of programs which are useful can be proven to halt for instance. Or you can just prove that the program is correct up to the point in time where the sun expansion covers the earth. There are often practical ways around such limitations, including the alteration or reformulation of the program.
the only thing halting problem says is that you can't prove *everything*
feel the difference between "any" and "every"
to stop being able to prove "every" thing you only need to 1 counterexample - which Turing found
all explicit examples of unprovable things are very removed from real demand (other than "prove arbitrary program halts", which probably doesn't count as real demand anyway and more of vapordream)
So if I have a language where I can encode in the type system that a number is a prime and is even, then for example the following would be a theorem with a proof:
Lemma even-prime: a -> Prime(a) ∧ Even(a) { // read as 'it returns a number `a` that is both prime and even
return 2
}
So they often have dependent type systems -- in these you can freely mix functions and values in your type signatures, not just types. E.g. you could have a Matrix type with two parameters, and then you can have functions like `transpose: Matrix a b -> Matrix b a`.
---
But this is just one side of the whole thing, the other is how to actually prove anything, like what even is `Even` in the above? A type like `someNum: Int` is also a theorem, but it only translates to "there exists an integer" - hardly interesting.
The real "mind blow" (at least to me) was that we just simply create a type for Equality. It takes the same parameter twice [1] (like in the Matrix example it would be Matrix a a) -- and thus we get a construct that can only be instantiated if the two sides are equal as per the language's compilers rules, that is automatically enforced by the compiler itself!
So now you can have `Eq 2 (1+1)`, but not `Eq 2 (1+3)`. And one last step that makes it general enough for all kinds of proofs, the compiler of these languages are not Turing complete. You can write many things, but for reasoning about loops you usually introduce a fuel that is always decreasing (and thus the compiler will accept it, as it knows it will run out once and that's enough for it). So it can evaluate everything, even in types and creating a normalized expression -- and then accepts everything as equal that normalizes to the same thing.
So for a more complex proof, you can just break down the problem to small steps that are by themselves understandably equal by the compiler.
[1] It's not quite true in this form
Proving that a particular program will or won't halt can still be easy.
The halting problem does imply that there exist programs which are entirely correct that lean will never be able to prove the correctness of, but this is not really relevant in practice.
This limits programs to the ones that can be formally shown to terminate. Which is good enough for most purposes.
My approach is to accept programs that run forever as long as I'm fairly sure each loop makes progress of some sort (instead of simply doing "while not solved: continue").
Edit: There's also a fun algorithm that, as far as I know, only provably terminates by being bounded by a sequence of strictly decreasing ordinals. Which breaks all kinds of models for proving it terminates.
On some programs like "stop" or "while(true)" the proof is easy.
With more sophisticated analysers it becomes possible on wider range of programs.
Why can't ai do this too? Is this the fundamental limit of ai?
E.g : Pegasus spyware don't break whatsapp crypto either
Im sure they allow bugs that benefit the NSA.
https://www.malwarebytes.com/blog/bugs/2026/10/signal-bug-co...
Downvote me, but yes I believe that Signal and the EFF are US military programs larping as civilian institutions.
Well the NSA is probably decent at building software.
It's not just total compensation. Working on classified stuff can be a bit of a career killer, since you can't talk about your past work when looking for a new job.
Plus there's the antipathy toward the current Trump administration, and the general moral unwillingness of many to do defense-related work in general.
Also, last I heard, cannabis use was still a disqualifier for DoD work and/or various security clearances. There are periodic ongoing polygraph tests, not sure about ongoing piss tests. The government is big; I'm sure the exact policies differ from department to department. But this turns a lot of people off.
Of course, every single thing I've said above might also be viewed as a positive by some engineers. Maybe they attract enough "true believers" to more than make up for the other factors.
US intelligence knows they can't go to policy makers and get funding for billion dollar domestic spy programs. So they stand up private companies and give them smallish grants at the beginning to get them on their feet, i.e Flock, Palantir, Signal Foundation, EFF, cloudflare, oracle. I could go on and on about orgs that their start off the back of US intelligence, whether through direct funding or through their alumni network.
The US Department of Defense has a long tradition of private public partnerships, but the privatization of intelligence has been accelerated in the last decade.
So while the NSA might not be able to attract talented SWEs for gov salaries to work on defense, their vendors that owe them their existence can.