I don't think Ada has anything like the Rust borrow-checker! A feature-set comparable to SPARK will need to wait until a better characterization of Rust Unsafe code is achieved, but in the long term it is absolutely a goal to be able to write Rust code that carries "contracts" for its use of unsafe features, and/or "proofs" that the code meets some specification.
Naturally since Ada is tainted by its history, other approaches more interesting to the common crowd are needed.