> SPARK itself can handle and prove some ownership properties but to the best of my knowledge isn't at the level of rust in memory safety on dynamically allocated memory.
And using https://www.adacore.com/sparkpro as a reference (ignore the 'Pro' bit as it's also available in the GPL edition) - anything certified to SPARK Silver level is far safer than any Rust code out there.