To oversimplify, this is a human workflow + LLM agent process that helped generate a formal specification, and then autonomously proved its equivalence to the semantics of a library in Signal (in...
To oversimplify, this is a human workflow + LLM agent process that helped generate a formal specification, and then autonomously proved its equivalence to the semantics of a library in Signal (in particular, on a single instruction architecture, for a single thread).
It should hopefully go without saying that this doesn't solve all bugs forever, but my hope is that it indicates the feasibility of generating similar proofs around some core security principles to prove the safety of the rest of the world's software + hardware stacks. Mostly useful for adjusting priors and all that for now.
It seems like it would imply that many kinds of "portable," source-code level bugs, which would work regardless of toolchain and architecture, are unlikely to exist, because they would have...
It seems like it would imply that many kinds of "portable," source-code level bugs, which would work regardless of toolchain and architecture, are unlikely to exist, because they would have affected the particular toolchain and architecture they tested? (Although, perhaps they are still possible because this toolchain might have done something that happened to remove some bugs.)
I wonder whether this Signal library is normally used on single or multiple threads? Proving things about concurrency bugs would be harder.
Hmmm. I'm not sure that I'd draw that conclusion myself. The goal was just to prove out some cryptographic + handshake protocol specifics (quoting the paper, "Signal’s post-quantum PQXDH handshake...
It seems like it would imply that many kinds of "portable," source-code level bugs, which would work regardless of toolchain and architecture, are unlikely to exist, because they would have affected the particular toolchain and architecture they tested? (Although, perhaps they are still possible because this toolchain might have done something that happened to remove some bugs.)
Hmmm. I'm not sure that I'd draw that conclusion myself. The goal was just to prove out some cryptographic + handshake protocol specifics (quoting the paper, "Signal’s post-quantum PQXDH handshake and Triple Ratchet, establishing forward secrecy, authentication, post-compromise security, and handshake secrecy") -- so, it would rule out truly massive compiler/toolchain issues that could affect another piece of software (like, pathological compiler stuff) but I doubt it'd catch anything spicy (like, speculative execution or some edge case in some combination of optimizers in clang).
IMO my main takeaways are that:
It took 6 million lines to do this, so as of 2026, still probably not doable for the average person,
It worked, and apparently got better over the course of execution (they found ways to optimize the pipeline), so we're probably very early in the ramp up phase for this sort of tech, and are likely to see more to come.
I wonder whether this Signal library is normally used on single or multiple threads? Proving things about concurrency bugs would be harder.
Oh, yeah, since they called out that it's only analyzing single threaded operation, it's almost certainly used concurrently in practice. And yeah that'll probably be another hurdle. Thankfully, software is the next best thing to free these days ...
To oversimplify, this is a human workflow + LLM agent process that helped generate a formal specification, and then autonomously proved its equivalence to the semantics of a library in Signal (in particular, on a single instruction architecture, for a single thread).
It should hopefully go without saying that this doesn't solve all bugs forever, but my hope is that it indicates the feasibility of generating similar proofs around some core security principles to prove the safety of the rest of the world's software + hardware stacks. Mostly useful for adjusting priors and all that for now.
It seems like it would imply that many kinds of "portable," source-code level bugs, which would work regardless of toolchain and architecture, are unlikely to exist, because they would have affected the particular toolchain and architecture they tested? (Although, perhaps they are still possible because this toolchain might have done something that happened to remove some bugs.)
I wonder whether this Signal library is normally used on single or multiple threads? Proving things about concurrency bugs would be harder.
Hmmm. I'm not sure that I'd draw that conclusion myself. The goal was just to prove out some cryptographic + handshake protocol specifics (quoting the paper, "Signal’s post-quantum PQXDH handshake and Triple Ratchet, establishing forward secrecy, authentication, post-compromise security, and handshake secrecy") -- so, it would rule out truly massive compiler/toolchain issues that could affect another piece of software (like, pathological compiler stuff) but I doubt it'd catch anything spicy (like, speculative execution or some edge case in some combination of optimizers in clang).
IMO my main takeaways are that:
Oh, yeah, since they called out that it's only analyzing single threaded operation, it's almost certainly used concurrently in practice. And yeah that'll probably be another hurdle. Thankfully, software is the next best thing to free these days ...