Great question. They don't have to trust the compiler: after compilation, they use an SMT-based proof process to establish that the resulting binary matches the semantics of the C source directly. See https://ts.data61.csiro.au/publications/nicta_full_text/6449....