Through a combination of mitigation of dynamic memory usage, borrow-checking analysis and advanced formal proof, SPARK formally demonstrates absence of memory issues such as use after free, access to uninitialized memory or memory leaks and corruption.
There is none as far as affine types go, even is there is a parallel to be made with limited types, but they don’t serve the same purpose.
The way Ada generally solves the same problem is by allowing much more in terms of what you can give a stack lifetime to, return from a function, and pass by parameters to functions.
It also has the regular « smart pointer » mechanisms that C++ and Rust also have, also with relatively crappy ergonomics
