iirc, SPARK has proof capabilities that outstrip the memory-safety guarantees of Rust. basically design by contract, where you can check loop invariants and statically verify complex preconditions and postconditions.

I suppose the workflow would be to flesh out and check the abstract design in something like Coq or (maybe) TLAPS, generate a refinement into the SPARK code contracts, then implement the functions. Since the toolchains are verified there shouldn't be much surface area for bugs left.