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.
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.