I am not a Rust expert either, but just a general remark: using a programming language like Rust as its intended to be used, i.e. functional/imperative programming of the problem domain, does not lend itself well to proving/disproving the kind of statements I showed above.

Yes, you could theoretically generate a Rust program that does not compile if some theorem does not hold, but this is often times (unless the theorem is about types) not a straightforward Rust program for the problem at hand.

I also think that, although Rust is blurring the lines a bit, equating formal verification and type-checking is not a valid stance. A type checker is a specific kind of formal verification that can operate on a program, but it will only ever verify a subset of all hypotheses: those about object types.