Great. Instead of telling us, most of whom already know, about it, go do it.

> Instead of fixing a particular use-after-free, how about making use-after-free impossible?

Yes ..

Does this vulnerability work only on a particular architecture?

The bug is architecture independent, although a particular exploit may work only on a specific architecture.

At what cost to performance? Very rarely are there solutions that exist without tradeoffs.

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.