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.
ane 2 hours ago [-]
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?
thibsrn 1 hours ago [-]
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.
Paracompact 1 hours ago [-]
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.
Or you can use verus instead which does automatic mapping from the rust code to the proof where possible.
Paracompact 52 minutes ago [-]
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.
vikramkr 1 hours ago [-]
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
philipwhiuk 1 hours ago [-]
Do you have some examples of this misaligned behaviour?
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?
VeejayRampay 49 minutes ago [-]
yeah it's nice and all but you're not providing evidence to back all those wild claims you're making
gigatexal 59 minutes ago [-]
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.
alexpadula 10 minutes ago [-]
Yeah ok. Look into the history a bit more if you think Google is clean.
1. AI Lean is not perfect and AI can easily cheat given it is writing the lean so the fact that the writeup didn't mention this is suspect and I will be reading the pdf to see what it says there. 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.
ghm2180 58 minutes ago [-]
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.
gregwebs 25 minutes ago [-]
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...
chriswarbo 43 minutes ago [-]
> 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.
breakwaterlabs 6 minutes ago [-]
> 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.
m_w_ 44 minutes ago [-]
> 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.
Mizza 2 hours ago [-]
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.
viraptor 1 hours ago [-]
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.
pmontra 1 hours ago [-]
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.
grumbelbart2 44 minutes ago [-]
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.
creata 23 minutes ago [-]
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.
vikramkr 1 hours ago [-]
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
112233 46 minutes ago [-]
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?
vikramkr 13 minutes ago [-]
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
saagarjha 58 minutes ago [-]
We're starting to get there with stuff like the compression thing.
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.
s08148692 2 hours ago [-]
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
vikramkr 1 hours ago [-]
Have seen that as well. A ton of the extra eng productivity has flowed into better eng practices
greenowl 44 minutes ago [-]
Any engineering layoffs? Still hiring? Frozen?
conartist6 2 hours ago [-]
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
Gasp0de 2 hours ago [-]
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.
wtetzner 36 minutes ago [-]
I think they were making a point about software in general, not just an encryption library.
jaimefjorge 21 minutes ago [-]
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.
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.
viraptor 1 hours ago [-]
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
tylerhou 20 minutes ago [-]
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.
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.
buckle8017 1 hours ago [-]
SGX is certainly completely broken.
Use s real password with the signal account thing.
fragmede 1 hours ago [-]
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.
ctrlaltdileep 1 hours ago [-]
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.
jchook 45 minutes ago [-]
It sounds like the Google team took a priori that Signal had a secure "cryptography core" and then published a result that validated that bias.
The proof shows that certain pre-determined properties hold, not that vulnerabilities do not exist. The approach cannot rule out attacks that the researchers did not anticipate.
For instance, the server software was merely simulated. Also it doesn't appear they evaluated the key generation portion of the system. Poorly generated keys or IVs can compromise a seemingly secure E2E system.
>> 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).
pvab3 1 hours ago [-]
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.
mapcars 53 minutes ago [-]
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.
ngruhn 1 hours ago [-]
I think we're well past that point anyway
throwaway198846 2 hours ago [-]
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.
Since code is cheap there is no excuse to not have verification everywhere.
whattheheckheck 2 hours ago [-]
How do you prove the lean code represents what the code its proving?
dinogo 46 minutes ago [-]
I feel that paradigms like this, is going to be the standard going forward.
xrisk 2 hours ago [-]
wonder how many dollars were spent on this
cicko 2 hours ago [-]
it was one-shotted last night when the new Fable came out
thereader12 2 hours ago [-]
It took 4 weeks according to the Article.
simon-ami 2 hours ago [-]
so, millions? billions?
yread 2 hours ago [-]
They thank Sundar Pichai. I guess it makes sense but at the same time...
tucnak 2 hours ago [-]
This is got to be an inside joke
nurumaik 2 hours ago [-]
Now pls do telegram to settle "telegram shouldn't have invented their own crypto" debate once and for all
pona-a 1 hours ago [-]
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.
whattheheckheck 2 hours ago [-]
"human experts work with AI to decide what to prove"
Why can't ai do this too? Is this the fundamental limit of ai?
afthonos 50 minutes ago [-]
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.
mjdiloreto 2 hours ago [-]
Because "what to prove" is fundamentally bound in a value judgment, not merely the mechanistic application of reasoning.
seydor 2 hours ago [-]
we are still involving humans in the loop, it helps them acquiesce
dmead 30 minutes ago [-]
did the formal proofs for the haskell compiler stop bugs from happening?
paganel 2 hours ago [-]
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)?
sebzim4500 2 hours ago [-]
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.
kuboble 2 hours ago [-]
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.
contravariant 2 hours ago [-]
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.
2 hours ago [-]
bananaflag 2 hours ago [-]
The same way Goedel's 0th incompleteness theorem doesn't make math proofs impossible (this is not sarcasm btw).
NooneAtAll5 2 hours ago [-]
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
bbor 2 hours ago [-]
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. :(
jlouis 2 hours ago [-]
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.
solyin 1 hours ago [-]
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?
NooneAtAll5 1 hours ago [-]
> 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)
xrisk 2 hours ago [-]
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
auggierose 2 hours ago [-]
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
gf000 1 hours ago [-]
> 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.
p-e-w 2 hours ago [-]
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.
Gasp0de 2 hours ago [-]
This didn't verify the Signal app, only the signal encryption protocol
the crypto might be secure; i wouldn't be so sure about the rest of the code.
hoppp 1 hours ago [-]
And it's never the crypto that breaks, it's usually something else.
E.g : Pegasus spyware don't break whatsapp crypto either
lifeisloving 2 hours ago [-]
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.
Downvote me, but yes I believe that Signal and the EFF are US military programs larping as civilian institutions.
psd1 2 hours ago [-]
White-listing contacts would have prevented the gaffe when a journalist was added to a war planning group
SiempreViernes 2 hours ago [-]
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.
booty 2 hours ago [-]
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.
lifeisloving 31 minutes ago [-]
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.
booty 15 minutes ago [-]
That's a great insight!
Computer0 2 hours ago [-]
I'm pleased to read Signal looks good to our robot mindlords.
58 seconds ago [-]
2 hours ago [-]
Rendered at 14:41:16 GMT+0000 (Coordinated Universal Time) with Vercel.
I wonder how this agent is different than a classic coding agent, in the end it seems to work the same way, iterating over a codebase while writing Lean or Rocq code and running it.
Or you can use verus instead which does automatic mapping from the rust code to the proof where possible.
Aggressively staggeringly high rates of straight up making shit up and covering up the lies. Gemini 3.5 flash was comical because it would delusionally scream nonsense like "we're go-go ready!!! :tada:" while the code didn't compile (I swear the only reason people thought that was a good model was because they didn't use it) and their models just got better at making tool calls without fixing it's tendency to cheat.
Gemini models are not looking all that good here: https://maxxbench.unlap.ai/
They got a lot of shit for it at the argon launch and you'll notice the carbon release blog has a lot of detail on how they focused on misalignme t and fabrication rates: https://blog.google/innovation-and-ai/models-and-research/ge...
So Google themselves is not behaving like they think people are making stuff up about their models behavior.
Google itself is also just behaving in such a sleazy way. "Carbon is the best model ever but also you can't use it yet." Watch them release it now that fable is out and nobody cares anymore so nobody checks to see how much they benchmaxed lol. They're clearly under some sort of internal pressure to pretend they're at the frontier and that's bleeding through I to the frenetic pace of model releases they've had in the past couple months through Argon and Carbon. Bleeding through in the sense of the models also only really care about benchmarks and good news cycles. Again they did claim they tried to solve a lot of this for carbon but they didn't let people use the model and once you have a base model that cheats benchmarks you have to wonder if it actually lies less or just gets caught less, but hopefully they got things back on track?
They all don't trust each other.
1. AI Lean is not perfect and AI can easily cheat given it is writing the lean so the fact that the writeup didn't mention this is suspect and I will be reading the pdf to see what it says there. 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.
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.
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...
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.
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.
It's going to take way more than throwing a more advanced LLM at the problem to make any progress.
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
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
> 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.
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 proof shows that certain pre-determined properties hold, not that vulnerabilities do not exist. The approach cannot rule out attacks that the researchers did not anticipate.
For instance, the server software was merely simulated. Also it doesn't appear they evaluated the key generation portion of the system. Poorly generated keys or IVs can compromise a seemingly secure E2E system.
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.
Why can't ai do this too? Is this the fundamental limit of ai?
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.
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.