Do you need everything to be PCC or can you use a secure kernel that supports confinement (e.g. EROS, L4sec) and then run whatever you want inside that?

Confinement would certainly be one way of getting "theorems for free" about untrusted code. But it doesn't work for all types of things you might want to prove.