Rust's borrow checking algorithm has been formally proven for a subset of the full language. Although this is one of those places where intuition is adequate to show the value, i.e. of enforcing exclusive mutability. After all, the intuition and implementation came before the proof (as is often the case).