[johnisgood]

> SPARK_Mode => Off is the SPARK equivalent of unsafe in Rust

As I said before: structurally, yes - both mark an implementation as opaque to the verifier/compiler. Semantically, though, SPARK is proof-driven: the verified interface still generates obligations for all callers, and the off-proof body is modularized. Rust's `unsafe` lifts restrictions, but does not automatically enforce correctness across the boundary. That distinction is why SPARK can provide whole-program, machine-checked guarantees while `unsafe` only shifts responsibility to the programmer.

... but I have already said this.