I don't think we can call it "automatic handling", you just play by the borrow checker's rules. Automatic are the garbage collectors but not Rust's model.

Anyway, you can verify the critical part of your C/Ada program by using: Why3 http://why3.lri.fr/ Frama-C http://frama-c.com/ (which is also extensible) SPARK https://www.adacore.com/about-spark

One company that I've worked for used generators, they were specifying the model with a DSL and they generated the code based on that. Can't give more information about that but there are others doing the same (SpaceX and NASA). Rust is very good for people that don't have the resources and money to throw at or are working in an industry where they don't need a certification, for example I have friends at Amazon in Romania that build Firecracker, a virtual machine that is supposed to improve the safety story on AWS Lambda.

And as an answer for your second question, at what cost? Also we don't know if Rust gets the scaling right. The compiler is already slow for the size of projects we already have.

There's a bit of disjoint between what those tools do and they what Rust does. Rust provides something different - you write the source in standard code and get a sound app. Verifiers can't do that with C. You essentially either write a parallel list of annotations or generate the app from another language. It's a valid approach, but that's why I objected to "exactly the same thing".

True, I'm familiar with ones in Java but not in C/C++. Having written a leak / double free detector for C, I have to say, you can only do so much statically and that wouldn't give me peace of mind exactly.

Frama-C and Microsoft's Security Description Language.