Rust has what we often call a "lightweight" formal method. These are those with simpler types of specification and/or more automated use. They tend to be quite

Rust has what we often call a "lightweight" formal method. These are those with simpler types of specification and/or more automated use. They tend to be quite specialized since that improves automation. The limited properties it proves are why it's so much easier to use than the general methods. 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.