In that case, one could just go with the semantics of the SPARK-like tool with equivalent algorithm, turn that to C or assembly, and use it with Rust's FFI. That's similar to my proposal for Rust + x86 Proved or TALC. This is also an area where formal specifications can have benefit showing intent for unsafe Rust and the proven replacement.
