I suspect Ada would make the cut, with the number of times it's been referenced in these contexts, but I haven't actually taken the time to learn Ada properly. It seems like a language before its time.
As I understand it it's only memory safe if you never free your allocations, which is better than C but not an especially high bar. Basically the same as GC'd languages but without actually running the GC.
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.
- https://alire.ada.dev/
- https://learn.adacore.com/
- https://pyjarrett.github.io/programming-with-ada/