It would seem but it's actually the opposite with existing tooling thanks to COGENT. Amateurs did a filesystem with a fraction of the work that pro's did the kernel:

https://ts.data61.csiro.au/projects/TS/cogent.pml

Note: See "Cogent: Verifying high-assurance file system..."

They leverage the same tools used for seL4 verification. Also worth noting that Myreen et al's toolkit basically converts HOL specifications to machine code without need for an external compiler. The "C" that was compiled was an embedding of it in HOL called Simpl which the aforementioned process verifies and converts to verified code. This is called translation validation. That's my non-specialist understanding of what the papers said. COGENT builds on this process to convert functional language and easier specs into that form which gets trans-validated into machine code. With less effort. :)

Note: Myreen et al are doing both verifications of HOL itself and HOL to hardware translation next. These further reduce the TCB of provers and hardware respectively to almost nothing but the specs.

Not really, to verify C code you need to set the compiler and its corresponding version in stone for the verification process, as UB can change even between versions of the same compiler.

Not really true. See https://www.nicta.com.au/publications/research-publications/... for how the compiler and its internal semantics are completely removed from the chain for l4v.

Thanks for the link, I will have a look into it.

Exactly, and then one has to deal with the runtime and GC.