alt Hacker NewsSomething seems wrong here. They took a non-trivial piece of human-written code that has had bugs in the past, formally verified the whole library, and found zero bugs?
I can believe that it's possible to get the LLM to write proofs, but I can't believe there were zero bugs in the system they verified. I wonder if they got the theorems wrong, or if they only proved narrow properties of the system.
I've had Claude formally verify crypto and data storage formats. It wrote theorems that looked fine and the formal verification passed but the resulting code contained many, many bugs that other implementations of the same things found with ad hoc testing.
The way the announcement is written, we should expect zero bugs in libsignal moving forward, and I guess time will tell whether that happens or not.
> they only proved narrow properties of the system.
It's that, yes.
They didn't prove that the code has no bugs; they proved that none of the current bugs (known or unknown) are security-breaking bugs, per their formalized security model.
> First, our researchers collaborated with a mix of models to translate Signal’s security goals into formal mathematical specifications, with human experts reviewing every one. From there, agents powered by Gemini Carbon did the proofs, generating over six million lines of Lean, a computer language that mathematically proves the accuracy of code.
The generated Lean code here is just being checked against the "formal mathematical specifications of Signal's security goals", not checked for the low-level properties you might care about as a programmer, e.g. "will it ever leak memory" or "will it ever crash", etc. And in fact, it's not even being checked for the reachability of non-security-violating protocol failure states, e.g. "could the protocol ever deadlock".
It's still perfectly possible for the code to have all of these problems. It's now just known that, as of the moment they did this analysis, none of those low-level problems, as far as they exist in the codebase, can cause a security-model violation.
Or, to put that another way: the system has been proven to "fail safe" in all its current failure modes, per their specific definition of safety (which is basically "keeping to the security guarantees Signal markets itself to users as having".)