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.