The security guarantees of existing verified compilers for compartmentalized programs in unsafe languages like C stop at a rather high-level, assuming a built-in protection mechanism and a block-based memory model. Verifying a concrete, low-level protection mechanism for compartmentalization is still a major challenge for current proof techniques. In particular, Abate et al.’s proof technique fails because one of their proof steps, recomposition, essentially requires hiding the code of each compartment. We propose an extension of their proof technique that allows verifying a more concrete low-level backend where compartments can observe each other’s code. To do so, we introduce an overlay semantics that allows us to characterize these observations as a form of undefined behavior, and we use a novel variant of recomposition that we call blame-aware recomposition. Essentially, blame-aware recomposition allows recomposing executions as needed in the high-level proof technique, even if the low-level context observes the code, because this context is ultimately going to be discarded.