On 30 Jan 2021, at 08:26, Bora Agca mailto:agca.software@gmail.com> wrote: Hi, i have one question: since the seL4 was written with a C compiler and it is possible that this compiler has an in-built backdoor, how can you still claim, that seL4 is "safe", i.e. non-hackable. because we prove that the binary is a correct translation of the verified (formalised) C. The compiler is definitely *not* part of our TCB. [ATM this is true for Armv7 only, but that part of the verification will be completed for RISC-V soon.] The white paper (https://sel4.systems/About/seL4-whitepaper.pdf) explains this on p 9–10. Gernot