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.

It's not free software (the license permits educational and research but commercial use). I guess selling compilers to people is a hard problem in itself. :)

It doesn't support all of C99 [1]. In real-world code, you need that, plus the GNU extensions (the clang developers put in a lot of work into making clang fully compatible with gcc, going as far as accepting the same command-line switches).

1 - http://compcert.inria.fr/compcert-C.html#subset

It's not a drop-in replacement for gcc. For example:

In the second form above, main is called with argc equal to zero and argv equal to the NULL pointer. The program does not, therefore, have access to command-line arguments.

http://compcert.inria.fr/man/manual004.html#toc11

For one you can still write buggy software in it and for another there are some limitations that can be potential deal breakers: http://compcert.inria.fr/compcert-C.html. That links spells out some of the limitations.