As people keep saying, one only has to verify functions that <i>can</i> break invariants, e.g. if you define a type that has invariants needed by `unsafe` blocks, then one has to take a close look at any functions that can modify its internals (i.e. things inside the module the type is defined).<p>Functions that can&#x27;t break these invariants because they don&#x27;t have access to the internals of a type do not need to be checked: they can be assumed safe.<p>&gt;  Well, given the most common refute of my concerns is &#x27;you just have to make sure your unsafe blocks are verified to be correct&#x27;, and the point of this article, is explicitly that this isnt the case...<p>And, as my comment says twice, my point is just that the two cases are not very different: verifying all unsafe blocks and verifying the modules that contain `unsafe` aren&#x27;t that different.