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.

The main cost to performance is related to multicore proofs. It is an open question on how to work out complete proofs of multithreaded operations.

This is why seL4 does not support internal SMP. You can run an instance per core and assign it a separate memory space like to a VM though.