I believe verifier is fine with unsafe code. Also not sure what does it have to do with defined/undefined behavior. Even if it is not verifiable, the behavior

I believe verifier is fine with unsafe code. Also not sure what does it have to do with defined/undefined behavior. Even if it is not verifiable, the behavior is still defined.