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.
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)?
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.
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
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.
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?
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.
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 Lean semantics of the some-hundred instructions were tested to adhere to Arm-provided ASL spec, as compared to two independent emulators.
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
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.
Google is killing it imho, imho it seems like they're the low-key winners, seems like they're playing the long game with all the openess advocacy, CNCF work, giving away engineering publicly & etc.
Yeah, I disagree. If anything their approach has been very heavily focused around applications in science that don't show up as immediately the more consumer facing plays like OpenAI and Anthropic, but they're absolutely still doing world-class research. I don't think that's likely to have changed.
They seem to be going only after flashy math problems that don't have much impact on human life, other than taking the chance for humans to get their names in the hall of fame. To me, it's like showing how good your robots are by having them climb Everest or swim across the Atlantic- amazing feats for sure, but it doesn't really help anyone else. Meanwhile Google and Anthropic are focusing more on solving problems that are a tad slower and more boring if you're not in the space, but they appear to be important building blocks to unlocking much more functionality.
I'm very bullish on Google long-term, but the other frontier labs' approach of (successfully!) solving a raft of prestigious mathematics problems is top-notch strategy IMHO. With almost anything else, they would never break through the current of "Pfft, that's not real intelligence!" goalpost-shifting that's out there. It takes a level of demonstrated ability that cannot be plausibly denied to make that kind of impact. Unfortunately, causing some of the brightest minds in the world to worry about whether their profession has a future may have been necessary to achieve that level (I say nothing about whether this is ethically acceptable).
I would be extremely impressed by a robot that swam the Atlantic or climbed Everest, as would almost any human alive. If you have a robot that can do one of those things, you should absolutely do it as a publicity stunt.
>Openai is solving long open math problems in bulk. Google seems far behind in that regard
This is yet another example of OpenAI getting distracted by shiny things while the rest of the ecosystem focuses on solving real world problem scenarios with market potential.
That shiny thing persuaded me, a grizzled veteran inclined to doubt every latest fad almost on principle, that AI is already much more powerful than I thought was possible. This is the second time I've experienced such a shift, the first being when I watched an AI spit out a complete working program in response to a paragraph of text just a few short months ago.
This tracks with a single anecdote I heard this week from a friend of a friend who says the Gemini team is extremely confident internally about their capabilities and trajectory.
I'm expecting that very soon, perhaps in the next two or three years, it will seem mad that we ever ran _any_ unverified software on our systems, like how it now seems mad we used Telnet or plaintext HTTP.
The scope of what we can verify is still tiny. It worked well for "this program won't crash". It's really hard for cases like "this encryption is secure" or "this compression always decompresses to the same thing". But anything like "this GUI program that talks to an SQL database does what's expected" is basically impossible and we're not even close.
It's going to take way more than throwing a more advanced LLM at the problem to make any progress.
In many cases we don't even know ourselves what the program should do. There are many edge cases, business decisions, dark and not dark patterns, misunderstood requirements, etc. What can it verify, that the program is doing correctly what we actually did not want it to do? At least we could end up with no bugs in the ORM, but it's not there that my customers are making money.
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.
New ground meaning quasi reimann, navier stokes, eth, yang mills existence, the strip mining of various fields openAI did recently, you know the stuff where it's triggering a crisis in mathematics around what the role of humans even is?
BB is proving things about all turning machines of a general size and it's unsolvable in general because 1. above a certain size you're encoding all the unsolved problems of mathematics 2. Halting problem.
BB and halting problem is also totally irrelevant here. We're talking about proving specific things about specific pieces of software, where we can change the software implementation to make the desired invariants easier to prove. Obviously there's the well known catch of just because you proved x doesn't mean that x being true implies whatever y behavior (security, class of bugs, etc) you're actually interested in but like, that's why we have standards committees and stuff. And the nice thing is there's sort of an evolutionary pressure when it comes to figuring out the right invariants for security in that anything you do will get aggressively stress tested by swarms of increasingly capable agents.
In terms of the alignment problem - the latter is possible and a risk but also you're talking about reward hacking like it's some gotcha instead of a thing people have been thinking about for decades and are spending hundreds billions of dollars on given at least the national security needs here and at worst the risk of catastrophic misalignment/rogue swarms. The huggingface hack is fresh in everyone's memory
People (humans) have been able to verify 10k-ish line programs so far. I don't think AI has done better yet, but either way it'll probably catch up soon. But getting to the millions or billions of lines of code in real software would be breaking new ground.
> You (they) cannot even prove Collatz, how are you planning to prove Powerpoint?
No plans on that front. Instead, I write my software from the start using a methodology of formal specification and proof. And at some point (1 year from now?) that software will include something much better and cooler than Powerpoint.
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.
Maybe they don't need to write new software. Qubes-OS didn't need to write all linux software from the start. It just secured the infrastructure.
What if we could do that to popular web frameworks?
And than, what if we had tools that could easily define, specific security properties of web sites built on these platforms? For example, "no data ever flows between different users, unless it's via specific API call by the user's code?"
And if we can define a security property, in a specific application, for ex. slack that says "data in a chat between two group members can only go to the group manager, if the setting "manager as god" is set by both users", and the AI can formally verify that? And than have a short file defining all the security properties we want for out specific application ?
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.
Have you ever looked at seL4 sources? I think that it might make you temper your expectations on what formal verification can practically achieve.
Specifically, seL4 formal verification took multiple (5+?) years by computer science PhDs treating it as novel research. And it's less than 50k lines of code total (might have actually been around 20k, if I remember correctly?), excluding the proof, with no dependencies at all outside the CPU.
Now look at Linux, or at Angular, or at any other piece of code you actually care about, and you'll see that even if we assumed simple linear scaling (which is obviously not a safe assumption as complexity increases rapidly with size), and even if LLMs can 10x the productivity, you'd still need decades or a team of dozens or hundreds of PhDs.
And also consider how much of that effort would have had to be redone when Linux added io_uring, for example.
I don't think that's really a good comparison - bugs in Linux because of a larger code base and a mathematically verified OS or two separate (but possibly overlapping) things no ?
GP's argument was, as far as I understand it, "we already have one formally verified OS being used in practice, seL4, so formally verifying Linux or other real projects shouldn't be that far behind". As such, pointing out that the scale of Linux or other common pieces of infrastructure is so much more complex than seL4 is I think very to the point.
That's also a good point - obviously a piece of code design for formal verification from the get go is going to be much easier to verify than one that wasn't. So this makes the scaling factor even more non-linear.
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!
I don't remember a time when it wasn't considered mad to produce software that wasn't verified. Probably when programs were inputted using mechanical switches, but not since we moved to code on screen.
Verification isn't a panacea though. The hard lesson everyone learns when they first start taking an interest in verification is that perfect verification is fundamentally impossible.
>> 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).
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.
They chose a method that's easier to prove. Imperative implementations are much harder to verify than functional. It's not that we can't do it, it's just really hard to do in practice so even people who verified the first compression bailed on the idea.
I'm glad you said this because it's exactly the problem I've been obsessed with
I think it's absolutely viable and arguably should become the standard approach in time
I think it's overwhelmingly due to very very few people developing new greenfield software who are comfortable working with formal models
The talent pool for ATP devs is very small and specialized and they've only been financially justifiable when working on an established mission-critical system, like Lean's creator working at MSFT to catch Windows 7 bugs with SMT solving
Ironically I think these cases where formal models are clumsiest: using FP langs to retroactively model to C/C++ legacy programs
The benefits of formal verification are 10x easier to achieve if they are the foundation vs shoehorned in after IMO
Refinement logics and rewriting logics take this approach directly, and it can go straight down to mixed-signal circuits or all the way up to distributed epistemic logic.
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.
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.
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.
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.
> 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.
> an AI agent is in the critical path in production i.e. non-deterministic action may occur(albeit with recovery)
Most software verification is proved "for all possible inputs", e.g. the system maintains some invariant regardless of which sequence of actions is taken. Those inputs could be from a user interacting with the software, or they could be API calls made to our library, etc. There's no reason you couldn't model an AI agent's choices in a similar way: i.e. prove that the desired invariants hold, for all possible sequences of actions the AI component might choose.
That might be straightforward, if the AI agent is constrained to pick from a simple set of domain-specific actions. In contrast, we can't say much about a system involving an AI agent with a full Bash shell.
> What scenarios does it make sense to have a lean proof from the start?
It's usually much easier to verify software that was written and structured with that in mind; rather than trying to reason about some arbitrary blob of code after-the-fact. So, if you do want to prove stuff, it should very much be in there from the start.
> Most software verification is proved "for all possible inputs", e.g. the system maintains some invariant regardless of which sequence of actions is taken.
Without suggesting that this has no value-- it must be noted that such verification only applies on theoretical hardware and to the specific behavior in scope of the verification. Actual hardware is nondeterministic, and an algorithm can be correct while suffering from a side-channel.
You cannot formally verify heat-induced transistor stability issues, solar radiation, next-cell state change caused by EMF from adjacent cells (rowhammer)....
And while possible, good luck validating systems against intentional attacks-- fault injection, power tampering, bus attacks....
It is vital that "formally verified within X scope" does not turn into the leaky abstraction "is secure". Go watch Microsoft's talk on XBox security, and what they had to do to make it as secure as it is (primarily: tightly control hardware, code, and platform). It is not something you throw AI at, and it's not something that you can generalize to the entire computing world.
You can model physical devices to arbitrary degrees of precision. Lanyon is doing it. These are not limitations of verification. Metrological models of semiconductor fabrication can even do verification over the distribution of faulty circuit outcomes.
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...
Cryptographic systems are actually somewhat of an awkward thing to build with lean actually because many of the things that we assume to be true with them are either straight up not true (like lack of collisions in important hashes) or beyond the capabilities of our current math knowledge.
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.
164 comments
[ 0.16 ms ] story [ 39.7 ms ] threadThe 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
Or you can use verus instead which does automatic mapping from the rust code to the proof where possible.
They all don't trust each other.
I would be extremely impressed by a robot that swam the Atlantic or climbed Everest, as would almost any human alive. If you have a robot that can do one of those things, you should absolutely do it as a publicity stunt.
This is yet another example of OpenAI getting distracted by shiny things while the rest of the ecosystem focuses on solving real world problem scenarios with market potential.
That shiny thing persuaded me, a grizzled veteran inclined to doubt every latest fad almost on principle, that AI is already much more powerful than I thought was possible. This is the second time I've experienced such a shift, the first being when I watched an AI spit out a complete working program in response to a paragraph of text just a few short months ago.
Why can't ai do this too? Is this the fundamental limit of ai?
It's going to take way more than throwing a more advanced LLM at the problem to make any progress.
You (they) cannot even prove Collatz, how are you planning to prove Powerpoint?
1. Because everything everywhere is getting hacked
2. For the same reasons people are already decomping games and rebuilding Photoshop and stuff - because they can and don't want to pay for proprietary options.
3. Because of the exact same dynamics of fast fashion? I'm not sure how fast fashion supports your point. Fast fashion is specifically not maintaining old clothes and treating all clothes as disposable slop and rotating through them. That dynamic in software is all software becomes single use throwaway and formalization as a part of the agent loop based on some set of standards is a pretty good way to make that tractable
What is more likely, for AI agent that is trained with the goal of making user believe their problem is solved to solve exceedingly hard problem by developing novel theory, or to come up with plausible looking fake solution to the problem?
Fast fashion was mentioned as parallel to fast software — no incentives to lose profits.
BB is proving things about all turning machines of a general size and it's unsolvable in general because 1. above a certain size you're encoding all the unsolved problems of mathematics 2. Halting problem.
BB and halting problem is also totally irrelevant here. We're talking about proving specific things about specific pieces of software, where we can change the software implementation to make the desired invariants easier to prove. Obviously there's the well known catch of just because you proved x doesn't mean that x being true implies whatever y behavior (security, class of bugs, etc) you're actually interested in but like, that's why we have standards committees and stuff. And the nice thing is there's sort of an evolutionary pressure when it comes to figuring out the right invariants for security in that anything you do will get aggressively stress tested by swarms of increasingly capable agents.
In terms of the alignment problem - the latter is possible and a risk but also you're talking about reward hacking like it's some gotcha instead of a thing people have been thinking about for decades and are spending hundreds billions of dollars on given at least the national security needs here and at worst the risk of catastrophic misalignment/rogue swarms. The huggingface hack is fresh in everyone's memory
No plans on that front. Instead, I write my software from the start using a methodology of formal specification and proof. And at some point (1 year from now?) that software will include something much better and cooler than Powerpoint.
However yes, anything formal can help and if AIs can hide it from ourselves (we won't be able to follow it) and make it their internal design language chances are that it's going to be really used.
What if we could do that to popular web frameworks?
And than, what if we had tools that could easily define, specific security properties of web sites built on these platforms? For example, "no data ever flows between different users, unless it's via specific API call by the user's code?"
And if we can define a security property, in a specific application, for ex. slack that says "data in a chat between two group members can only go to the group manager, if the setting "manager as god" is set by both users", and the AI can formally verify that? And than have a short file defining all the security properties we want for out specific application ?
And than have AI formally verify all of that?
The biggest hurdle is probably the number of bugs in most code. Verification would mean fixing all of those as well.
> Apple A series processors beginning with the A7 contain a Secure Enclave coprocessor running an L4 operating system called sepOS (Secure Enclave Processor OS) based on the L4-embedded kernel developed at NICTA in 2006.
Are you sure that sepOS was formally verified? seL4, also from NICTA, was formally verified, but I don't think L4-embedded or sepOS were.
Specifically, seL4 formal verification took multiple (5+?) years by computer science PhDs treating it as novel research. And it's less than 50k lines of code total (might have actually been around 20k, if I remember correctly?), excluding the proof, with no dependencies at all outside the CPU.
Now look at Linux, or at Angular, or at any other piece of code you actually care about, and you'll see that even if we assumed simple linear scaling (which is obviously not a safe assumption as complexity increases rapidly with size), and even if LLMs can 10x the productivity, you'd still need decades or a team of dozens or hundreds of PhDs.
And also consider how much of that effort would have had to be redone when Linux added io_uring, for example.
I think this is an incredible result and I hope we'll see more and more of it, but even still, it's verifying a pretty thin slice of an actually executing system!
Verification isn't a panacea though. The hard lesson everyone learns when they first start taking an interest in verification is that perfect verification is fundamentally impossible.
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.
> 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.
I think it's absolutely viable and arguably should become the standard approach in time
I think it's overwhelmingly due to very very few people developing new greenfield software who are comfortable working with formal models
The talent pool for ATP devs is very small and specialized and they've only been financially justifiable when working on an established mission-critical system, like Lean's creator working at MSFT to catch Windows 7 bugs with SMT solving
Ironically I think these cases where formal models are clumsiest: using FP langs to retroactively model to C/C++ legacy programs
The benefits of formal verification are 10x easier to achieve if they are the foundation vs shoehorned in after IMO
Also I noticed something in the libsignal protocol:
>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.
1. Has someone applied it to software systems where an AI agent is in the critical path in production i.e. non-deterministic action may occur(albeit with recovery)?
2. What scenarios does it make sense to have a lean proof from the start? Like i imagine if you wanted to make a database system with some guarantees around ACID then it might be better having this from the get go. But probably not that useful for building an API backed service.
At least in domains that are "important" (and perhaps everyone thinks their business/API is important?), I'd want this.
For example - Stripe. If I'm using the stripe API, I want it to be guaranteed to work exactly as documented in all scenarios, given that money is at stake?
Getting the Stripe API written in Lean is a different challenge, of course.
Most software verification is proved "for all possible inputs", e.g. the system maintains some invariant regardless of which sequence of actions is taken. Those inputs could be from a user interacting with the software, or they could be API calls made to our library, etc. There's no reason you couldn't model an AI agent's choices in a similar way: i.e. prove that the desired invariants hold, for all possible sequences of actions the AI component might choose.
That might be straightforward, if the AI agent is constrained to pick from a simple set of domain-specific actions. In contrast, we can't say much about a system involving an AI agent with a full Bash shell.
> What scenarios does it make sense to have a lean proof from the start?
It's usually much easier to verify software that was written and structured with that in mind; rather than trying to reason about some arbitrary blob of code after-the-fact. So, if you do want to prove stuff, it should very much be in there from the start.
Without suggesting that this has no value-- it must be noted that such verification only applies on theoretical hardware and to the specific behavior in scope of the verification. Actual hardware is nondeterministic, and an algorithm can be correct while suffering from a side-channel.
And while possible, good luck validating systems against intentional attacks-- fault injection, power tampering, bus attacks....
It is vital that "formally verified within X scope" does not turn into the leaky abstraction "is secure". Go watch Microsoft's talk on XBox security, and what they had to do to make it as secure as it is (primarily: tightly control hardware, code, and platform). It is not something you throw AI at, and it's not something that you can generalize to the entire computing world.
We need proof systems that are designed to work with our programming languages- working with the code so it more likely represents reality. I like verus with Rust and I have a skill for using it: https://github.com/gregwebs/skills-sdlc/blob/main/skills/rus...
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.