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