It's not a mathematical proof in the literal sense (yet), because there are known soundness bugs in Rust that are yet to be addressed; moreover the interaction of borrow checking (including interior mutability) with the traits system is poorly understood and has not been proven to be correct even in a simplified model. It should yield a meaningful level of checking, and if nothing else, the ergonomics is way better than just running a static analysis on C/C++ code (setting aside the question of whether current static analysis tools can even check for possible data races); but you shouldn't rely on it to that extent.