Many verification systems can understand virtually any proof you can throw at them, so any memory management scheme for which you have a rigorous argument for correctness should be able to operate with no additional runtime overhead. And if you don't have such an argument, you've already lost no matter what language you use.