These claims aren’t contradictory when you understand the domain in question: formal verification of C abstract semantics doesn’t scale particularly well. Rust (and Ada) both have restricted memory semantics (particularly around aliasing) that effectively eliminate some of the hardest problems in whole-program static analysis.