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.
Re:AlphaProof Code
by pcthrowaway on Tuesday November 10, 2026 @10:55PM
(#50449578)
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")
Proofing and securing those is the way larger attack vector and work to come.