Capability machines are promising targets for secure compilers since capabilities can be used to enforce abstractions that are usually expected for high-level languages, such as well-bracketed control-flow (WBCF) and local state encapsulation (LSE). We present the first formalization of a capability machine that supports mechanized reasoning about deep semantic properties, including WBCF and LSE. Our formalization is done in the Coq implementation of Iris, a state-of-the-art concurrent higher-order separation logic, and includes a formalization of the logical relation defined by Skorstensgaard et al. [ESOP2018], which can used to prove WBCF and LSE.