Compcert is guaranteed to compile correct C code to correct assembly (given its TCB assumptions). It doesn't say anything about incorrect C code. So in order

Compcert is guaranteed to compile correct C code to correct assembly (given its TCB assumptions). It doesn't say anything about incorrect C code. So in order to benefit from CompCert, first you have to prove that you have valid C in the first place, which is no easy feat. You'd probably be better off using a language that's designed with verification in mind, like Cogent or ADA/Spark, or waiting for lambda-Rust to become production ready, since in those cases you won't have to prove tedious bureaucratic memory safety invariants for the vast majority of your code, and can focus on functional correctness (or, if you just care about memory safety, you can stop there).