Right. The problem is that those languages are relatively permissive in their type systems. Obviously Rust can capture more in its type system than C can. You would probably want a type like “decreasing unsigned integer” for Rust and some way to enforce monotonic decreasing, which Rust doesn’t give you.

(Any experts on formal verification please correct any inaccuracies in what I say here.)

The upshot of it is that C, C++, and Rust permit too much behavior that isn’t capturable in the type system. Thus, the properties that you’re interested in are semantic (as opposed to syntactic; type systems turn semantic properties into syntactic ones) so Rice’s theorem applies and there’s no computable way to do the analysis right.