>>lacksc+(OP)
We do have formal proofs of various security properties at the architectural level that consider the entire architecture with all its complexities and warts. Speculative execution is of course a concern (and is an active area of research for us), though our belief is that the bounds information now present at the hardware level allows it to be tamed. Another concern is the interaction between undefined behaviour and CHERI; the former needs to be sufficiently constrained in order to not inadvertently turn code that would be memory safe with a naive CHERI compiler into code that is not. We also know there are still memory safety-like issues we can't protect against; we can stop pointer injection, but we can't stop tricking programs into copying the "wrong" pointer somewhere, or type confusion bugs that result in using pointers in an unintended way. Many of those exploit chains today rely on exploiting some other memory safety vulnerability we do protect against, but we cannot predict if people will come up with alternative approaches that avoid those in a world with CHERI.