We contribute a new approach for secure compilation of verified C code that we conjecture to be fully abstract. The approach relies on target language support for capabilities: a well-studied form of unforgeable memory pointers that enables fine-grained, efficient privilege separation. Such capabilities are implemented in special processors called capability machines, particularly the recent CHERI processor. More specifically, we rely on support for sealed capabilities (like CHERI’s), as well as a form of capabilities called linear capabilities. Linear capabilities are specially treated by the hardware to ensure that they can never be copied. Using these target-language security primitives, our compiler relies on information from both the source program and its verification proof, i.e. it will be formally defined as a separation-logic-proof-directed compiler.