Yes, CompCert is no timeless perfect gem. You could make a convincing argument that it's not really verified software in the Djikstra mold at all (only parts of the compiler are verified, although they are fairly large and interesting parts).

It does make a nice poster child for formal methods though.