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