The formal C semantics are defined in Isabelle/HOL, checked, and then the compiler output is also checked. They use standard GCC compilers for all of this.

See https://riscv.org/blog/2021/05/sel4-on-risc-v-verified-to-bi...