You don't have to formally verify the entire module. The module "just" has to be correct :P. Additionally, very often, unsafe code is used in ways that cannot

You don't have to formally verify the entire module. The module "just" has to be correct :P. Additionally, very often, unsafe code is used in ways that cannot contaminate the entire module (that's the ideal, in fact), and the module that the unsafe code is used in is made deliberately small.