> they only proved narrow properties of the system.

It's that, yes.

They didn't prove that the code has no bugs; they proved that none of the current bugs are security-breaking bugs, per their formalized security model.

> First, our researchers collaborated with a mix of models to translate Signal’s security goals into formal mathematical specifications, with human experts reviewing every one. From there, agents powered by Gemini Carbon did the proofs, generating over six million lines of Lean, a computer language that mathematically proves the accuracy of code.

The generated Lean code here is just being checked against the "formal mathematical specifications of Signal's security goals", not checked for the low-level properties you might care about as a programmer, e.g. "will it ever leak memory" or "will it ever crash" or "will it ever deadlock", etc. It's still perfectly possible for the code to do all of those things; it's just known that, as of the moment they did this analysis, none of those low-level problems will cause a security-model violation.

Or, to put that another way: the system has been proven to "fail safe" in all its current failure modes, per their specific definition of safety.

Well I’m not even sure they did that. Not really.

They took signals security goals/aim/target and used models to generate a mathematical model. Which is a bit “hey trust us bro” in 3 ways but they did have human experts fully review 1 path, partially review 1 path, and the last I’m not really sure.

The fully reviewed path was that the aims goals were turned into positive mathematical statements “we will achieve X Y Z” so if we trust the humans that part should be as strong as we achieved X Y Z.

Tons of lean code generated to prove X Y Z correct, a lot of it is entirely self consistent. But then because it’s too much to look at we had the AI judge all of it for problem areas and we had humans look at that 1% of it… okay? That’s great if your magic box can pick out the problem areas but that wasn’t proved.

My last issue is, and please tell me if I’m wrong or missed something, but what says or proves the security goals/models are necessary and sufficient? We aim to do X Y Z. Great. We aim to not do A B C. not sure if I’m quibbling or this is strictly needed but it seems missing (unless it can be captured in entirely in the positive statement) let’s assume it’s included. We did X Y and Z, we did not do A B or C. Okay what’s my prize? Unbreakable crypto?

“Um well no… we know we can have X Y and Z while not having A B and C”

And so if we have X Y Z none of A B C we know the model is good.

“Yeah, probably”

And that the code at some point in time is no better than that?

“Yeah, certainly”

We may be able to say that X Y and Z are necessary since I can show you a concrete attack if you omit one. But we can never be absolutely certain that they're sufficient. Still, we've had something like 30-40 years of research by now looking at how to specify security properties. We certainly didn't get many things right the first time around. For the "basic" stuff, like confidentiality and authenticity we likely have a reasonably good grip on it under some, let's say "reasonable" assumptions. But a lot of research also still goes into developing notions of security with weaker assumptions or more exotic goals.

Note that this is about Signal’s cryptographic protocol, not the Signal App or the surrounding platform OS.

Proofing and securing those is the way larger attack vector and work to come.

I applaud them for starting with the protocol, because that can be generalized beyond any one specific implementation in principle, even if, in practice, we're somewhat limited to the official Signal apps given their centralized nature. Securing the applications themselves (perhaps starting with their implementations of the protocol, but the rest is also fair game) will inevitably be a bigger task.

I'm actually unclear on whether they just translated the design of the protocol to Lean, or translated the app's implementation of the protocol to Lean.

The wording of the article is a bit too ambiguous to say either way, I think? They just say they "generated" the Lean code; they didn't say what it was being generated from.

From this I think it's a given that they were talking about the implementation, not the specification

> To confirm that AlphaProof Code can tell correct code from buggy code, we reintroduced two real, previously fixed bugs into an isolated version of Signal's code. In both cases, the system produced a machine-checked proof that the buggy version was insecure.

is it just the protocol? Or is it also "the part of signal that implements the protocol", at least, yes it does what it's supposed to, with no weird timing collisions when multithreaded?

Also, I presume there are some unproved baked in assumptions about cryptographic primitives (e.g, but not necessarily, "sha512 has a uniform distribution")

I guess we need to define what bugs are.

Software doesn't exist in a platonic state like formal mathematics, which at least can be consistent with all other results. Software interacts with the real world and "bugs" can be any number of security weaknesses like emitting useful timing signatures, buffer overflows that depend on the compiler used, weaknesses on certain hardware, etc.

It is great that Google has formalized code to some degree and for software that MUST be hardened, this may be valuable. It may be generally useful, but we need to get a feel for the gaps that inevitably will persist.

> Software doesn't exist in a platonic state like formal mathematics

Doesn't it? Like all these things you can model in the end, your state space, and thus necessary proofs and even just the spec itself would explode in size.

But that's how every single model works.

You'd just move from bugs in code to bugs in the spec.

Real software needs mind blowingly complex specifications and while it's now fairly easy to get an AI generated proof that your code follows the spec, there's not much to help you with bugs in the spec.

AI will happily change the spec for you so the code verifies though, but that doesn't solve the trust issue.

Truly a trusting trust scenario.

I have recenctly tried to move my codebase more to spec driven development, but I aborted it. For my use case it felt wrong. It just creates drift and more prose explaining what I need.

I’m not saying I’m right, but I want to understand. What’s the benefits of raw specs with AI, when AI can read the source of truth and explain to you?

The thesis is that you can come up with a tight spec that defines what correctness means for you. Then the AI writes lean proofs that your code follows this spec.

In practice, for real systems, this much moves source of truth, as you have pointed out.

However, there is a clear 'compactness' advantage for specs.

Specs can either define the operational (what it does) or the denotational semantics (what it is) for a system, while the code can only be operational. Some things are just easier and better defined in denotational semantics.

> it's now fairly easy to get an AI generated proof that your code follows the spec

It's my understanding that automatic tools were able for a while already to verify whether a given system (code or otherwise) adheres to a given formal specification (at one point after the Pentium bug debacle AMD had its FPU proven, there are variants of the L4 microkernel which were proven, etc.).

The (great) challenge remained to create a formal specification from something humans can write and understand. Isn't that were LLMs come in? And isn't that were the current trust gap remains?

Hey wanna tryna flip hundreds into thousands??

This is true for all formal verification systems, though. You can only formally prove that code does what a spec says, you can’t verify that a spec perfectly matches what the code is intended to do.

Well, arguably if you generate your code from the spec itself then it could be possible.

But even then, what's not possible is to "know" whether the spec=code is whatever the creator actually had in mind.

But still, the target programming language's formalism is still likely done on a higher level, than e.g. its compiler output on a given CPU, so compiler bugs could still "throw a wrench" into the system.

Or CPU bugs/flaws, or…

This seems like a trivial thing to verify though, point it at a known software version with a CVE, like OpenSSL / Heartbleed, or some of the more recent SSL / PHP / Node / HTTP issues. Then you would expect it to find the Heartbleed vulnerability quite quickly. If it does not, investigate and iterate.

This is not a "verify my code" kind of product, it takes real human work from experts in software verification but makes it possible for those experts to work on larger codebases.

So this wouldn't prove as much as you think. Especially since both tge experts and the LLMs behind this are well aware of Hearbleed - so them finding Hearbleed wouldn't tell you anything, really.

> They took a non-trivial piece of human-written code that has had bugs in the past, formally verified the whole library, and found zero bugs?

Well, if it's SSH then I sure hope it has no LLM-discoverable bugs.

[delayed]

> if they only proved narrow properties of the system.

It's always this. Basically, the big issue with proof systems is that you have got to decide yourself what you want to prove. When someone say software is formally proofed, the first question you should ask is what was proven.