Yeah but aren't these formal proof methods a lot more general, and thus more widely applicable? In other words, does Rust provide the right balance between security and complexity?
Also note that the problems the borrow checker handles are really hard to do safely in general without overhead. They're hard to test for and debug, too. So, the use of a limited logic with automation just for that makes sense. It's why the other tools for C code were developed, too. Before that, people were using things like SPIN model checker for such things. Again, that looks like overkill to get just a few safety properties vs Rust's built-in method that's simpler.