microkit
microkit copied to clipboard
Document what kernel proofs apply
Those who are not super familiar with seL4 may pick up the Microkit assuming that it is using the verified configuration when in reality currently that is not the case. This is primarily due to MCS not being verified as well as other specific option such as allowing SMC calls on ARM platforms.
Somewhere in the manual, we should be clear about this.