I am pretty sure the CVE would probably be raised against C/C++ as a whole, considering that the language itself allows these kinds of things to happen in the first place lol (I know this is an unfair comparison given that one could probably TECHNICALLY write correct and safe code in it, but you get my point). Granted, Rust allows unsafe too, but at the very least it does its very best to contain these sorts of things. It's a LOT better
Anyways, this quote before really drives the point home.
In C/C++ something is correct when someone can use it correctly, but in Rust something is correct when someone can't use it incorrectly.
That would be this paper. To my knowledge this is indeed coming to Ada, and they are also working on interesting Prusti-style reasoning principles for SPARK. This will be interesting to see -- in terms of verifying functional correctness, Ada is still way ahead of Rust, so we might be able to learn some things from them.
For example the string functions like strncpy(). Which sounds like it copies a string to a string. Except when it is allowed to produce an output that is not a proper null terminated string. strcpy(3) - Linux manual page