4 ms·
> seL4 is the only microkernel that has a proof of correctness ProvenCore (https://provenrun.com/provencore/ https://provenrun.com/provencore/) has a proof tha
by el_pollo_diablo 2y ago
> seL4 is the only microkernel that has a proof of correctness
ProvenCore (https://provenrun.com/provencore/ https://provenrun.com/provencore/) has a proof that covers correctness (memory safety, and more generally absence of UB, termination, etc.), functional properties (e.g. the fork() system call is a refinement of an abstract "clone" operation of abstract machines), and security properties (memory isolation).