This is not a counter-example to the claim you are citing. If you added this form of `evil` to `Vec`, then since `evil` is within the module, the proof of corr

This is not a counter-example to the claim you are citing. 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. Of course, if `len` were public, that would be a different story. Unsafety doesn't pollute beyond module boundaries if all the extra invariants are about private fields.