Something seems wrong here. They took a non-trivial piece of human-written code that has had bugs in the past, formally verified the whole library, and found zero bugs?
I can believe that it's possible to get the LLM to write proofs, but I can't believe there were zero bugs in the system they verified. I wonder if they got the theorems wrong, or if they only proved narrow properties of the system.
I've had Claude formally verify crypto and data storage formats. It wrote theorems that looked fine and the formal verification passed but the resulting code contained many, many bugs that other implementations of the same things found with ad hoc testing.
The way the announcement is written, we should expect zero bugs in libsignal moving forward, and I guess time will tell whether that happens or not.
Great, what a great use case for AI. I feel like Google has been the cleanest of the big players in terms of useful contributions and control of their AI systems. This new proof agent doesn't seem to challenge the spec though, just the implementation, if I've understood correctly.
I wonder how this agent is different than a classic coding agent, in the end it seems to work the same way, iterating over a codebase while writing Lean or Rocq code and running it.
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
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?
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.
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.
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.
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!
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.
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?
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.
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.
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.
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.
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.
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.
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...
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.
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.
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).
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.
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.
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.
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.
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?
They all don't trust each other.
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.
It's going to take way more than throwing a more advanced LLM at the problem to make any progress.
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!
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.
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.
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.
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.
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.
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...
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.
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
https://verity.md/benchmark#calcom
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.
> 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.
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).
Since code is cheap there is no excuse to not have verification everywhere.
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.
On some programs like "stop" or "while(true)" the proof is easy.
With more sophisticated analysers it becomes possible on wider range of programs.
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.
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:
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. :(
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)
And just to add, this is also true of "human" mathematics as well.
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.
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.