It does have support for formal verification though unlike most languages.
Technically, it used to be memory safe before this and they rolled back the restrictions to allow "unchecked deallocation".
Pointers ("Accesses") are also typed, e.g. you can have two incompatible flavors of "Widget*" which can't get exchanged which helps reduce errors, and pointers can only point at their type of pointer unless specified otherwise, are null'd out on free automatically and checked at runtime. In practice, you just wrap your allocations/deallocations in a smart pointer or management type, and any unsafe usages can be found in code by looking for "Unchecked" whether "Unchecked_Access" (escaping an access check) or "Unchecked_Deallocation".
The story is quite different in Ada because of access type checks, it doesn't use null-terminated strings, it uses bounded arrays, has protected types for ensuring exclusive access and the language implicitly passes by reference when needed or directed.
My experience with writing concurrent Ada code has been extremely positive and I'd highly recommend it.