Sounds a bit like Microsoft's Singularity project, though I don't know if they even used a proof system to ensure a program couldn't do bad stuff(TM). After verification they just let the program run in Ring 0 (kernel space) of the CPU to skip even the performance hit of the cpu's isolation.