seL4 – микроядро, реализующее интерфейс микроядер семейства L4 и прошедщее формальную верификацию. Собственно ядро написано на языке C, а формальная верификация проведена с использованием Isabelle.
- Comprehensive Formal Verification of an OS Microkernel