Hacker News Reader

Comment by ane | Hacker News Reader

How is guaranteed that whatever the compiled Rust code running on a Lean model of a processor is doing matches what a real processor is doing? How do we know that the Lean spec that it wrote based on the specification matches what the Rust code that implements Signal does?

View on HN

This article is not saying that AI did the proof magically. Their statement is quite clear, the agent system helped human experts for the proof, going back and forth at different steps. The complexity came from the size of the codebase and the compiled implementation, which an AI-assisted process was able to tackle at much greater speed than a meat-only team of experts would have. The experts are still responsible for designing the mathematical specifications, and maybe along the way something was wrongly designed, but I still feel much safer about Signal's architecture and implementation.

Rust need not apply, since the proof is about the libsignal-cli ELF binary, compiled under reasonable assumptions (single-threaded, statically linked, etc). The semantics of the some-hundred instructions in their language in Lean were tested to adhere to Arm-provided ASL spec, as compared to two independent emulators.

It's not and we don't. We can however run some lean in rust with things like https://github.com/conao3/lean-rs

Or you can use verus instead which does automatic mapping from the rust code to the proof where possible.

Not sure why you're responding with information that would imply they modeled Rust in Lean or vice versa. As I explained, their target was the compiled ELF binary, not Rust source. This way, they avoid including the entire Rust compiler and its as-yet formally undefined semantics into the trusted computing base. They lose guarantees about any compiled Signal binary that is not bit-for-bit this one, though.

I mean typically the answer to this question should be that the underlying compiler has also been proven and both proofs cover a guarantee of no undefined behavior in either implementation

Reply on news.ycombinator.com