I don't think the definition of "memory safe" has ever required full end to end stack conformance with a proof. Very few languages have achieved that, though some have. Most people call Java memory safe, C#, Python, Typescript, etc - all of those fall short of a formally verified, sound type system with a verified toolchain.

Not to talk about Go, which has intentional unchecked-at-runtime UB (data races) yet many argue to consider it memory safe (and I have a feeling that the same people arguing Rust isn't memory safe are also there. Just a feeling though).