This is not a counter-example to the claim you are citing.<p>If you added this form of `evil` to `Vec`, then since `evil` is within the module, the proof of correctness has to cover `evil`. Doing that proof will fail. So, it is not necessary to look outside of the module to notice that something is wrong.<p>Of course, if `len` were public, that would be a different story. Unsafety doesn&#x27;t pollute beyond module boundaries <i>if all the extra invariants are about private fields</i>.