We formalize a programming framework that advocates programming systems like TEEs as a collection of compartments that access separate memory locations and conform to a public interface. We propose an approach that leverages compartmentalization to bring security-relevant properties verified at the source level down to the binary via certified compilers. Compartmentalization at the source level allows us to establish the desired properties over every concurrent execution of a program by verifying each compartment in isolation. To preserve compartmentalization at the target level and benefit from its compositional behavior, we define interface-preserving compilers, which preserve the structure and properties of compartments when compiling them in isolation. We show that CASCompCert, in particular, is interface-preserving.