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.
> they only proved narrow properties of the system.
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?
This is true for all formal verification systems, though. You can only formally prove that code does what a spec says, you can’t verify that a spec perfectly matches what the code is intended to do.
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.
This seems like a trivial thing to verify though, point it at a known software version with a CVE, like OpenSSL / Heartbleed, or some of the more recent SSL / PHP / Node / HTTP issues. Then you would expect it to find the Heartbleed vulnerability quite quickly. If it does not, investigate and iterate.
You'd just move from bugs in code to bugs in the spec.
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.
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.
Google is killing it imho, I'm with a thesis they're the lowkey winners of the race and know it and maybe are comfortable not making too much of a fuss about it, seems like they're playing the long game with all the openess advocacy, CNCF work, giving away engineering publicly & etc.
How is guaranteed that whatever the compiled Rust code running on a Lean model of a processor is doing matches what a real processor is doing? How do we know that the Lean spec that it wrote based on the specification matches what the Rust code that implements Signal does?
This article is not saying that AI did the proof magically. Their statement is quite clear, the agent system helped human experts for the proof, going back and forth at different steps. The complexity came from the size of the codebase and the compiled implementation, which an AI-assisted process was able to tackle at much greater speed than a meat-only team of experts would have.
The experts are still responsible for designing the mathematical specifications, and maybe along the way something was wrongly designed, but I still feel much safer about Signal's architecture and implementation.
Rust need not apply, since the proof is about the libsignal-cli ELF binary, compiled under reasonable assumptions (single-threaded, statically linked, etc). The semantics of the some-hundred instructions in their language in Lean were tested to adhere to Arm-provided ASL spec, as compared to two independent emulators.
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.
I mean typically the answer to this question should be that the underlying compiler has also been proven and both proofs cover a guarantee of no undefined behavior in either implementation
Agreed. This doesn’t read like the hype most ai firms put out. Google is using it like a tool. The human review of the 1% that matters is really smart.
Unfortunately their Gemini models are dangerously misaligned and lie like crazy because they've been desperately benchmaxing them, and the crap they're pulling with AI overview and search in schools etc is pretty bad. But outside their Gemini and search lines yeah they've been pushing useful boundaries with protein stuff/stuff like alphafold etc. But inside Gemini they've been taking good advantage of their reputation as a responsible don't be evil tech player to be a lot worse than openai and Anthropic
Not the OP, but I was asking gemini about a Google subscription I had, trying to figure out whether I would lose a particular feature if I changed the subscription. I asked whether my subscription was "grandfathered" and it assured me it was not, then later on acknowledged that I was on a legacy subscription that I would not be able to go back to.
Compared to the other LLMs I've used, it seems to have system instructions that are far more adversarial to the user.
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.
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?
Very cool. A couple of years back I was toying with the thought of developing a specialized model for formal verification using something like the AlphaZero approach. Given the news from the past few months now I'm glad that I didn't, it really seems that general purpose LLMs are eating everything.
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.
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!
Because, people keep confusing proofs with theorems. The proof can be correct, while the theorem is the wrong one. And if you got the wrong theorem, you might not be interested in its proof (sometimes you are, anyway).
The nice thing is that a theorem doesn't have to completely describe the software, it can just describe some property you care about.
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.
Well, property tests exist and in some cases they are better soslution than other types of test.
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.
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 scope of what we can verify is still tiny. It worked well for "this program won't crash". It's really hard for cases like "this encryption is secure" or "this compression always decompresses to the same thing". But anything like "this GUI program that talks to an SQL database does what's expected" is basically impossible and we're not even close.
It's going to take way more than throwing a more advanced LLM at the problem to make any progress.
In many cases we don't even know ourselves what the program should do. There are many edge cases, business decisions, dark and not dark patterns, misunderstood requirements, etc. What can it verify, that the program is doing correctly what we actually did not want it to do? At least we could end up with no bugs in the ORM, but it's not there that my customers are making money.
Right. The paper notes that they stubbed out all the trickier crypto and system call routines with contracts. If those routines don't adhere to the modeled contracts in real execution, then the proof's guarantee won't hold. Also things like concurrency and signal handling are intentionally not modeled.
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!
Why? We already have formally verified microkernels in production (Apple's L4 variant in their security enclave, for example). I'd say the tools are mostly there, it's a matter of scaling, and maybe a matter of adapting code to make verification easier. Both things where LLMs can shine.
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.
The thing about exponentials is that we can go from "we're not even close" to "all software in the world was getting aggressively hacked and we figured it out to stop that from happening" very very quickly. I would not be surprised if by this time next year we had some sort of nist standard for formal verification or something. It certainly changes things a lot once llms can solve millennium problems
You speak as if that is a software or tech problem. People cannot even stop producing direct-to-garbage fast fashion. Who can make them completely rewrite all software, so it is tractable to prove? Please consider that there has been almost no hardware nor llm architecture progress in last few years. Apparent progress is people literally burning money to buy and power the gpus.
You (they) cannot even prove Collatz, how are you planning to prove Powerpoint?
Maybe they don't need to write new software. Qubes-OS didn't need to write all linux software from the start. It just secured the infrastructure.
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 ?
Claiming the models are not good at math at this point, especially for things like formalization where w you aren't even breaking new ground, is a very very bold claim to make. So ignoring that point for obvious reasons, why would people rewrite all software?
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 do you mean "no new ground"? There is a very narrow, super constrained set of programs that we know how to formalize, some programs we kinda sorta hope we can, and absolutely everything else where we might not even bother. Check out what epic effort it took to prove 5th busy beaver. no visible abvances on collatz conjecture - and those are among simpliest things you can come up with! Any software that embeds similar behaviour is undecidable by construction. Which forces a rewrite to exclude such behaviour. Or, most likely, fabricating proof criteria that are unsound.
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.
New ground meaning quasi reimann, navier stokes, eth, yang mills existence, the strip mining of various fields openAI did recently, you know the stuff where it's triggering a crisis in mathematics around what the role of humans even is?
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
People (humans) have been able to verify 10k-ish line programs so far. I don't think AI has done better yet, but either way it'll probably catch up soon. But getting to the millions or billions of lines of code in real software would be breaking new ground.
> You (they) cannot even prove Collatz, how are you planning to prove Powerpoint?
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.
That is actually impressive. And most likely the only way to get such software — by writing formally sound code from start. Trying to turn existing toilet pot into pot of gold "with AI" is modern alchemy.
I don't know if you comment was sarcasm. If not, how does your methodology specifies and proves that your Powerpoint replacement will draw rectangles with the fashionable gradients of the year you release it. If gradients won't have fallen out of fashion again by then. And that's only a silly example. Programs like that have a huge number of features. I am ready to bet that some of them have been designed and informally approved in front of a coffee machine 20+ years ago.
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.
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 have been writing my own programming language _completely in lean_, from the parser down to the compiler.
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...
I think the most interesting thing is that they loaded the compiled binary right into lean, if I'm understanding the technical paper correctly. Then they use ARM semantics as the base to prove other properties. That's really exciting that they went all the way to the binary level! It reminds me a bit of metamath-c, in that they verify every step of the process, all the way down to binary, so nothing in-between is missed.
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.
> an AI agent is in the critical path in production i.e. non-deterministic action may occur(albeit with recovery)
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.
> Most software verification is proved "for all possible inputs", e.g. the system maintains some invariant regardless of which sequence of actions is taken.
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.
You cannot formally verify heat-induced transistor stability issues, solar radiation, next-cell state change caused by EMF from adjacent cells (rowhammer)....
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.
A backend API service may have some core business logic or other properties that would be worthwhile to prove certain properties about.
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...
> 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.
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.
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.
Anecdotally in my company we have observed a far lower incident and outage rate since we moved to complete Agentic coding.
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
How often do you need to change the actual library which does the encryption for the signal protocol? Adding features to the app does not require changes to the encryption.
I mean, you setup a webcam at the top of your rented Colo rack space so that you know when the feds come to take your server to hack the SGX/equivalent.
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.
You can. It ends up really slow normally which is why we don't do it. For example for a proven Deflate, it took an hour to process a 1MB file https://ar5iv.labs.arxiv.org/html/1609.01220
That’s not a great source to support your claim. From the paper
> 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.
>> 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).
I do not understand how this is materially different to just asking <existing frontier model> to "rewrite <thing> in Lean", then check for verifiably unintended diffs.
Cheaper? Faster? More faihtful? Finds more defects in the source software? Unclear.
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.
Tested is one thing, proved is another. While you need less people to do this, now it also becomes meaningful to spend resources on, instead of another new feature.
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.
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)?
Solving the halting problem means writing a program which can tell whether an arbitrary other program will halt or not.
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.
Dijkstra's approach would be to prove there is a strictly decreasing natural number associated to the loop.
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.
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. :(
Driving a lean proof manually is a lot of effort. It's often 50x or 100x the effort of writing the initial program in the first place. The grand idea here is that if you can get a system to have a good heuristic/intuition for figuring out those proofs, you can lower this effort amplification by a lot. This makes formal verification at this level feasible for mission critical software, and also a larger slew of software we rely on.
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.
Which definition of singularity are you using? I'm still doing my own laundry. It's quite poetic, what you wrote, if a bit sad. The hours between birth and death are waste, but are to be enjoyed. To discover the human condition. Overcome adversity, or die trying. Yes the machine gods will reign supreme but until they come to be, we must play and feel joy and sadness and love, hate... sonder. The planet doesn't have to be a bunch of sad monkeys. Maybe you can make a virus that will turn us into joyous lizards! There is so much left to discover and understand. How do you un-fry an egg?
> Which means that they just luckily don't have to prove anything about any software that might halt...? Or?
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)
lean has no relation to the halting problem; you can think of it as a language that allows proofs to be encoded as code, and the compiler that runs that code as knowing how to enforce mathematical constraints appropriately
there certainly is a relation; you might not be able to prove all the properties you care about because of the halting problem; but that is more a theoretical problem, not a practical one
They haven't "invent their own crypto" (please don't make me visualize Durov inventing Diffie Hellman). They took the OTP protocol and cut it in all the wrong ways, gave up on multi-device other systems easily support, and reinvented TLS while putting device IDs outside the encrypted packet, leaking persistent IDs to LAN.
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.
Well the NSA is probably decent at building software. But none of this really matters if the OS isnt secure and the OS is much more complex and less verifiable. Also, why does the government use their own versions of Signal that are more secure, makes you wonder.
Would it? As I remember the journalist's number was added to an existing contact by some smart feature in iOS, not sure how a whitelist would help there.
Well the NSA is probably decent at building software.
Ultimately I'm sure they are but my secondhand understanding from friends is that it's difficult for the US gov't to attract and retain software engineering talent.
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.
I would argue that US intelligence, especially on the technical side of things has put emphasis on privatization of these sectors.
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.
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.
> they only proved narrow properties of the system.
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".)
Note that this is about Signal’s cryptographic protocol, not the Signal App or the surrounding platform OS.
Proofing and securing those is the way larger attack vector and work to come.
Well I’m not even sure they did that. Not really.
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”
This is true for all formal verification systems, though. You can only formally prove that code does what a spec says, you can’t verify that a spec perfectly matches what the code is intended to do.
I guess we need to define what bugs are.
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.
This seems like a trivial thing to verify though, point it at a known software version with a CVE, like OpenSSL / Heartbleed, or some of the more recent SSL / PHP / Node / HTTP issues. Then you would expect it to find the Heartbleed vulnerability quite quickly. If it does not, investigate and iterate.
> 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?
Well, if it's SSH then I sure hope it has no LLM-discoverable bugs.
You'd just move from bugs in code to bugs in the spec.
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.
Hey wanna tryna flip hundreds into thousands??
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.
Google is killing it imho, I'm with a thesis they're the lowkey winners of the race and know it and maybe are comfortable not making too much of a fuss about it, seems like they're playing the long game with all the openess advocacy, CNCF work, giving away engineering publicly & etc.
How is guaranteed that whatever the compiled Rust code running on a Lean model of a processor is doing matches what a real processor is doing? How do we know that the Lean spec that it wrote based on the specification matches what the Rust code that implements Signal does?
This article is not saying that AI did the proof magically. Their statement is quite clear, the agent system helped human experts for the proof, going back and forth at different steps. The complexity came from the size of the codebase and the compiled implementation, which an AI-assisted process was able to tackle at much greater speed than a meat-only team of experts would have. The experts are still responsible for designing the mathematical specifications, and maybe along the way something was wrongly designed, but I still feel much safer about Signal's architecture and implementation.
Rust need not apply, since the proof is about the libsignal-cli ELF binary, compiled under reasonable assumptions (single-threaded, statically linked, etc). The semantics of the some-hundred instructions in their language in Lean were tested to adhere to Arm-provided ASL spec, as compared to two independent emulators.
It's not and we don't. We can however run some lean in rust with things like https://github.com/conao3/lean-rs
Or you can use verus instead which does automatic mapping from the rust code to the proof where possible.
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.
I mean typically the answer to this question should be that the underlying compiler has also been proven and both proofs cover a guarantee of no undefined behavior in either implementation
Agreed. This doesn’t read like the hype most ai firms put out. Google is using it like a tool. The human review of the 1% that matters is really smart.
Yeah this is what people want, less hype, more "boring" but useful examples of a powerful tool.
Unfortunately their Gemini models are dangerously misaligned and lie like crazy because they've been desperately benchmaxing them, and the crap they're pulling with AI overview and search in schools etc is pretty bad. But outside their Gemini and search lines yeah they've been pushing useful boundaries with protein stuff/stuff like alphafold etc. But inside Gemini they've been taking good advantage of their reputation as a responsible don't be evil tech player to be a lot worse than openai and Anthropic
Do you have some examples of this misaligned behaviour?
https://www.nytimes.com/2026/11/05/technology/ai-safety-scho...
Not the OP, but I was asking gemini about a Google subscription I had, trying to figure out whether I would lose a particular feature if I changed the subscription. I asked whether my subscription was "grandfathered" and it assured me it was not, then later on acknowledged that I was on a legacy subscription that I would not be able to go back to.
Compared to the other LLMs I've used, it seems to have system instructions that are far more adversarial to the user.
Ask for “grandmothered” for a more forgiving response
Theo is quite the twitter shitposter but this tweet lines up directly with what I've seen: https://x.com/theo/status/2114483219538296946
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?
> Watch them release it now that fable is out and nobody cares anymore so nobody checks to see how much they benchmaxed lol
Fucking called it: https://blog.google/innovation-and-ai/models-and-research/ge...
yeah it's nice and all but you're not providing evidence to back all those wild claims you're making
Provided in reply to sibling comment
Yeah ok. Look into the history a bit more if you think Google is clean.
They all don't trust each other.
Very cool. A couple of years back I was toying with the thought of developing a specialized model for formal verification using something like the AlphaZero approach. Given the news from the past few months now I'm glad that I didn't, it really seems that general purpose LLMs are eating everything.
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.
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!
Because, people keep confusing proofs with theorems. The proof can be correct, while the theorem is the wrong one. And if you got the wrong theorem, you might not be interested in its proof (sometimes you are, anyway).
This.
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?
The nice thing is that a theorem doesn't have to completely describe the software, it can just describe some property you care about.
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.
Well, property tests exist and in some cases they are better soslution than other types of test.
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.
This is why I think tests are useless if written by AI. They will always pass and look reasonable.
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 scope of what we can verify is still tiny. It worked well for "this program won't crash". It's really hard for cases like "this encryption is secure" or "this compression always decompresses to the same thing". But anything like "this GUI program that talks to an SQL database does what's expected" is basically impossible and we're not even close.
It's going to take way more than throwing a more advanced LLM at the problem to make any progress.
In many cases we don't even know ourselves what the program should do. There are many edge cases, business decisions, dark and not dark patterns, misunderstood requirements, etc. What can it verify, that the program is doing correctly what we actually did not want it to do? At least we could end up with no bugs in the ORM, but it's not there that my customers are making money.
Right. The paper notes that they stubbed out all the trickier crypto and system call routines with contracts. If those routines don't adhere to the modeled contracts in real execution, then the proof's guarantee won't hold. Also things like concurrency and signal handling are intentionally not modeled.
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!
Why? We already have formally verified microkernels in production (Apple's L4 variant in their security enclave, for example). I'd say the tools are mostly there, it's a matter of scaling, and maybe a matter of adapting code to make verification easier. Both things where LLMs can shine.
The biggest hurdle is probably the number of bugs in most code. Verification would mean fixing all of those as well.
Wikipedia says:
> 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.
The thing about exponentials is that we can go from "we're not even close" to "all software in the world was getting aggressively hacked and we figured it out to stop that from happening" very very quickly. I would not be surprised if by this time next year we had some sort of nist standard for formal verification or something. It certainly changes things a lot once llms can solve millennium problems
You speak as if that is a software or tech problem. People cannot even stop producing direct-to-garbage fast fashion. Who can make them completely rewrite all software, so it is tractable to prove? Please consider that there has been almost no hardware nor llm architecture progress in last few years. Apparent progress is people literally burning money to buy and power the gpus.
You (they) cannot even prove Collatz, how are you planning to prove Powerpoint?
Maybe they don't need to write new software. Qubes-OS didn't need to write all linux software from the start. It just secured the infrastructure.
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?
Claiming the models are not good at math at this point, especially for things like formalization where w you aren't even breaking new ground, is a very very bold claim to make. So ignoring that point for obvious reasons, why would people rewrite all software?
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 do you mean "no new ground"? There is a very narrow, super constrained set of programs that we know how to formalize, some programs we kinda sorta hope we can, and absolutely everything else where we might not even bother. Check out what epic effort it took to prove 5th busy beaver. no visible abvances on collatz conjecture - and those are among simpliest things you can come up with! Any software that embeds similar behaviour is undecidable by construction. Which forces a rewrite to exclude such behaviour. Or, most likely, fabricating proof criteria that are unsound.
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.
New ground meaning quasi reimann, navier stokes, eth, yang mills existence, the strip mining of various fields openAI did recently, you know the stuff where it's triggering a crisis in mathematics around what the role of humans even is?
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
People (humans) have been able to verify 10k-ish line programs so far. I don't think AI has done better yet, but either way it'll probably catch up soon. But getting to the millions or billions of lines of code in real software would be breaking new ground.
The people don't produce fast fashion. The forces of capitalism encourage it.
> You (they) cannot even prove Collatz, how are you planning to prove Powerpoint?
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.
That is actually impressive. And most likely the only way to get such software — by writing formally sound code from start. Trying to turn existing toilet pot into pot of gold "with AI" is modern alchemy.
Amen.
I don't know if you comment was sarcasm. If not, how does your methodology specifies and proves that your Powerpoint replacement will draw rectangles with the fashionable gradients of the year you release it. If gradients won't have fallen out of fashion again by then. And that's only a silly example. Programs like that have a huge number of features. I am ready to bet that some of them have been designed and informally approved in front of a coffee machine 20+ years ago.
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.
We're starting to get there with stuff like the compression thing.
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 have been writing my own programming language _completely in lean_, from the parser down to the compiler.
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...
I think the most interesting thing is that they loaded the compiled binary right into lean, if I'm understanding the technical paper correctly. Then they use ARM semantics as the base to prove other properties. That's really exciting that they went all the way to the binary level! It reminds me a bit of metamath-c, in that they verify every step of the process, all the way down to binary, so nothing in-between is missed.
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.
> an AI agent is in the critical path in production i.e. non-deterministic action may occur(albeit with recovery)
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.
> Most software verification is proved "for all possible inputs", e.g. the system maintains some invariant regardless of which sequence of actions is taken.
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.
We can formally verify the Verilog or equivalent too.
You cannot formally verify heat-induced transistor stability issues, solar radiation, next-cell state change caused by EMF from adjacent cells (rowhammer)....
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.
A backend API service may have some core business logic or other properties that would be worthwhile to prove certain properties about.
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...
> 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.
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
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.
Anecdotally in my company we have observed a far lower incident and outage rate since we moved to complete Agentic coding.
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
Yes! For me, it has both freed up time to do more testing and verification, and also made those tasks significantly faster.
Have seen that as well. A ton of the extra eng productivity has flowed into better eng practices
Any engineering layoffs? Still hiring? Frozen?
it'll be much better once each CI run costs $10,000 for the AI to make sure you didn't break its giant proof
How often do you need to change the actual library which does the encryption for the signal protocol? Adding features to the app does not require changes to the encryption.
I think they were making a point about software in general, not just an encryption library.
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...
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/
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.
SGX is certainly completely broken.
Use s real password with the signal account thing.
I mean, you setup a webcam at the top of your rented Colo rack space so that you know when the feds come to take your server to hack the SGX/equivalent.
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.
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.
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.
You can. It ends up really slow normally which is why we don't do it. For example for a proven Deflate, it took an hour to process a 1MB file https://ar5iv.labs.arxiv.org/html/1609.01220
That’s not a great source to support your claim. From the paper
> 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.
There was recently a decently fast implementation of DEFLATE in Lean: https://kim-em.github.io/blog/2026-7-24-why-lean-is-faster-t...
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).
Saving man-hours is a big deal. Progress opens more and more doors, the main thing is not to open the last one.
I do not understand how this is materially different to just asking <existing frontier model> to "rewrite <thing> in Lean", then check for verifiably unintended diffs.
Cheaper? Faster? More faihtful? Finds more defects in the source software? Unclear.
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.
Tested is one thing, proved is another. While you need less people to do this, now it also becomes meaningful to spend resources on, instead of another new feature.
I think we're well past that point anyway
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.
some are https://www.crowdsupply.com/sutajio-kosagi/precursor caugh CPU-ish
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
it was one-shotted last night when the new Fable came out
It took 4 weeks according to the Article.
so, millions? billions?
They thank Sundar Pichai. I guess it makes sense but at the same time...
This is got to be an inside joke
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)?
Solving the halting problem means writing a program which can tell whether an arbitrary other program will halt or not.
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.
Halting problem only stops you from your prover from working on all programs.
On some programs like "stop" or "while(true)" the proof is easy.
With more sophisticated analysers it becomes possible on wider range of programs.
Dijkstra's approach would be to prove there is a strictly decreasing natural number associated to the loop.
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.
The same way Goedel's 0th incompleteness theorem doesn't make math proofs impossible (this is not sarcasm btw).
do you mean how is halting problem not a blocker or how halting problem itself is proven?
answer to the first is same as always - by simply not guaranteeing that everything is provable, especially in finite amount of time
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:
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. :(
Driving a lean proof manually is a lot of effort. It's often 50x or 100x the effort of writing the initial program in the first place. The grand idea here is that if you can get a system to have a good heuristic/intuition for figuring out those proofs, you can lower this effort amplification by a lot. This makes formal verification at this level feasible for mission critical software, and also a larger slew of software we rely on.
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.
Which definition of singularity are you using? I'm still doing my own laundry. It's quite poetic, what you wrote, if a bit sad. The hours between birth and death are waste, but are to be enjoyed. To discover the human condition. Overcome adversity, or die trying. Yes the machine gods will reign supreme but until they come to be, we must play and feel joy and sadness and love, hate... sonder. The planet doesn't have to be a bunch of sad monkeys. Maybe you can make a virus that will turn us into joyous lizards! There is so much left to discover and understand. How do you un-fry an egg?
> Which means that they just luckily don't have to prove anything about any software that might halt...? Or?
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)
lean has no relation to the halting problem; you can think of it as a language that allows proofs to be encoded as code, and the compiler that runs that code as knowing how to enforce mathematical constraints appropriately
there certainly is a relation; you might not be able to prove all the properties you care about because of the halting problem; but that is more a theoretical problem, not a practical one
> you might not be able to prove all the properties you care about
And just to add, this is also true of "human" mathematics as well.
Now pls do telegram to settle "telegram shouldn't have invented their own crypto" debate once and for all
They haven't "invent their own crypto" (please don't make me visualize Durov inventing Diffie Hellman). They took the OTP protocol and cut it in all the wrong ways, gave up on multi-device other systems easily support, and reinvented TLS while putting device IDs outside the encrypted packet, leaking persistent IDs to LAN.
"human experts work with AI to decide what to prove"
Why can't ai do this too? Is this the fundamental limit of ai?
Because humans are the ones who care? At some point, you have to make the wish, or the genie is not going to do anything.
Because "what to prove" is fundamentally bound in a value judgment, not merely the mechanistic application of reasoning.
Because that’s a design question. The AI has to know what it’s actually supposed to be building.
we are still involving humans in the loop, it helps them acquiesce
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.
This didn't verify the Signal app, only the signal encryption protocol
still a big codebase: https://github.com/signalapp/libsignal
Yeah quite impressive.
the crypto might be secure; i wouldn't be so sure about the rest of the code.
And it's never the crypto that breaks, it's usually something else.
E.g : Pegasus spyware don't break whatsapp crypto either
Well the NSA is probably decent at building software. But none of this really matters if the OS isnt secure and the OS is much more complex and less verifiable. Also, why does the government use their own versions of Signal that are more secure, makes you wonder.
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.
White-listing contacts would have prevented the gaffe when a journalist was added to a war planning group
Would it? As I remember the journalist's number was added to an existing contact by some smart feature in iOS, not sure how a whitelist would help there.
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.
I would argue that US intelligence, especially on the technical side of things has put emphasis on privatization of these sectors.
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.
That's a great insight!
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