C++ already gives us a tool for pointer zapping

Strictly speaking, we don't need CHERI to support non-strict provenance checking. We merely need it to answer honestly about whether two pointers are actually equivalent (substitutable, not just numerically equal) when we test them for equality, and we also need that behavior to carry over into its atomics.

Since I have already called out that I might be wrong about std::launder(), for the rest of this comment I am going to use the word "launder" to mean "whatever incantation causes the compiler to ignore provenance requirements for a given pointer, assuming that such an incantation exists or would be standardized." Under PVNI-plain, this incantation is a simple pointer-to-integer round trip, but I want to speak generally for all possible semantics and not just PVNI-ish semantics.

As for the LLVM thing, I think it depends on how this gets formalized. There are four-ish possible formalizations that I can think of:

0. Comparing pointers which have non-overlapping provenance is implementation-defined or UB, so LLVM's behavior is right (but maybe they still need to explicitly document it). In that case, we can't make any useful atomic<T*> data structure that works on CHERI (and possibly not even on conventional hardware) unless the compiler provides a language extension explicitly supporting it. Even laundering probably doesn't help in all cases because atomics do not (currently) provide an API to say "do a compare-exchange, but atomically launder your stored value first."
1. Pointers with non-overlapping provenance may compare as equal or unequal. Such a comparison has no effect on provenance. This probably also makes atomics unworkable without laundering, but at least now we're not looking at nasal demons.
2. Pointers with non-overlapping provenance must compare as unequal, but the implementation may choose to arbitrarily launder any pointer at any time, in which case it may compare as equal to any other pointer to an object at the same address. In other words, the compiler may arbitrarily pretend that a pointer has been laundered wherever it so pleases, but it must be consistent. Once the implementation launders a pointer, that pointer must stay laundered for future operations (but not past operations - the implementation is explicitly *not* required to "go back in time" and launder any other pointers that were ever compared with a given pointer, so my earlier concern about the transitivity of == would not apply here). Believe it or not, I think this probably can be implemented on CHERI-with-honest-pointer-comparisons (as described above), simply by configuring the compiler to never optimize the result of a pointer comparison to anything other than unequal (if you can prove that the provenances do not match, then they compare unequal, otherwise let the hardware sort it out, meaning that it returns true on regular hardware and false on CHERI, and that's OK because both results will cause the program to behave acceptably on their respective platforms). This would possibly require some additional tracking on the part of the compiler to ensure that it is consistent about its reasoning with respect to provenance, but I don't see this as unduly burdensome. We're not asking the compiler to solve the halting problem or anything, just don't insert optimization X unless you have already applied optimization Y to the same code.
3. Pointer comparisons must fully respect provenance. Pointers must compare equal if and only if they have the same provenance (or at least overlapping, as in the case of array element pointers) and are numerically equal. This is the most correct behavior, but I suspect it defeats some optimizations and/or would require compilers to explicitly track provenance at runtime (on non-CHERI hardware), both of which are less than ideal.