Even ignoring the licensing issues and limited subset of C supported, the code quality doesn't approach that of modern optimizing compilers, and the correctness proof doesn't include things like concurrency or actual machine memory models (although forks of CompCert exist for some of these), so you're still off in the unverified world if you rely on them in your code.

Also, for the vast majority of programs the possibility of bugs in the compiler is not really that impactful in terms of total effect on reliability.