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