&gt; I&#x27;ll take your word on the smart pointers doing bounds-checks as I&#x27;m not up-to-date on all the techniques of C++ developers. Academics need to do a fresh take on that with assessments vs particular risks &amp; compared to current languages.<p>That&#x27;s kind of already happened. Stroustrup has done a whole ton of work in that area with Concepts.<p>&gt; Meanwhile, most in safety-critical development that I know of don&#x27;t use C++ because it&#x27;s too complex and unsafe per them.<p>It turns out that provable correctness invariably involves a fair bit of complexity (you are basically compiling a mathematical proof). People use Haskell and Coq to really do it right, and --surprise-- those turn out to be hard for programmers to learn.<p>A lot of other, more popular, high level languages are actually terrible for provable correctness, even if they are better for proving memory safety. C++ isn&#x27;t as effective for the job, but it has the advantage of being great for integrating in with the platform. It is a trade off, but one that is well worth while.<p>&gt; So, do you have any resources showing that C++ code is safe and analysable if one just uses smart pointers?<p>This stuff goes back a way, but stemmed from Modern C++ Design. There is a whole world of policy based design where you use the type system (much as with Haskell and Coq) to enforce declarative policies.<p>The quick thought experiment would be something like this:<p><pre><code>    template &lt;class T&gt;
    struct SafeRef {
        void check() { ... }
        operator T&amp;() { check(); return *x; }
        operator const T&amp;() const { check(); return *x; }
    private:
        T* x;
    };
</code></pre>
You can override operator-&gt; to make it behave more like a proper pointer. CRTP gives you some pretty powerful ways of getting the job done too.