seL4
seL4(secure embeded L4 Microkernel)
セキュアでマイクロカーネルかつRTOS
Isabelle/HOLを使った証明がある
#OS #形式手法 #Coq