> But the original claim is that it is all statically checked in Rust
Where? The GP's comment says "prefers," which I didn't read to mean a blanket statement. I don't think anybody with more than passing experience in Rust (or C) would make such a claim.
> Some dependently types languages can prove this statically, also model checking can do this, etc. So it can be done statically as well, but not in Rust.
You're couching the part where it can't be done with full generality or can be done with full generality, but with punishing semantics. The appropriate comparison here is with other normal general purpose compiled languages.
I read "Rust prefers to prevent all undefined behavior statically," to also imply that it actually does this, because otherwise the word "all" would not make sense to me in this sentence.
Dependently types languages and model checking do exist. They come with tradeoffs, but this is also true for Rust.