The verification sees the entire C code for one particular combination of configuration options. Currently this is the imx6 platform, Cortex A9 processor, ARMv7-a architecture, all other config options unset (in particular DEBUG, PROFILING, etc). Excluded from this C code is the machine interface and boot code, their behavior is an explicit assumption to the proof.
You can further inspect the gory details by looking at the preprocessor output in the file kernel_all.c_pp in the proof build - this is what the prover, the proof engineer, and the compiler see after configuration is done. So a quick way of figuring out if something is in the proof input or not is checking if the contents of that file change if you make a change to the source you’re wondering about. You don’t need the prover for this, and only parts of the seL4 build environment setup.
The top-level proof makes statements about the behaviour of all of the kernel entry points, which we enumerate once manually in the proof. The prover reads in these entry points, and anything that they call must either have a proof or an assumption for it to complete its proof. If anything is missing, the proof fails.
That means all of the C code that is in this kernel_all.c_pp file either:
- has a proof,
- or has an explicit assumption about it,
- or is not part of the kernel (i.e. is never called)
The functions with explicit assumptions are the machine interface functions mentioned above (they’re usually inline asm) and the functions that are only called by the boot process (usually marked with the BOOT_CODE macro in the source so they’re easy to spot).
As an example, the CPU and architecture options mean that everything under src/arch/ia32 is not covered by the proof, but that the files in src/kernel/object are.