gcc is not part of the TCB, thanks to our binary verification toolchain, which proves that the compiler/linker output retains the semantics of the C code. This means our proofs extend to to the executable code.
We did years ago experiment with CompCert. It resulted in performance degradation. But furthermore, using CompCert would not give us a complete proof chain. It uses a different logic to our Isabelle proofs, and we cannot be certain that its assumptions on C semantics are the same as of our Isabelle proofs.