It&#x27;s not practical to formally verify everything. We&#x27;d get nothing done if that was the case.<p>Rust&#x27;s memory safety promises can be reasoned about clearly without formal verification (which is an arduous process requiring a team of researchers -- basically what RustBelt is doing). This is enough to be convinced that Rust is protecting you from memory corruption. Formal correctness proofs are valuable, but not <i>necessary</i> to ship software.<p>Also, as others have mentioned, Rust is a strict plus over C++ in formal verification as well since once you&#x27;ve verified a module containing unsafe code, you can forget that it contains unsafe code and use it wherever, and modules with safe code can be used without verification. Once verified, Vec&lt;T&gt; is safe to use however you want as long as it&#x27;s not used in an unsafe block (if it is, just verify that block or module depending on the context).