microkit icon indicating copy to clipboard operation
microkit copied to clipboard

Document what kernel proofs apply

Open Ivan-Velickovic opened this issue 9 months ago • 0 comments

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.

Ivan-Velickovic avatar Apr 09 '25 06:04 Ivan-Velickovic