seL4
보안과 신뢰성이 극도로 중요한 환경을 위해 설계된 마이크로커널이다. 세계 최초로 소스 코드 수준에서 정형 검증이 완료된 운영체제 커널로, 정형 기법 연구의 대표적인 벤치마크 대상이다.