He mentions the seL4 microkernel. The specification is written in Isabelle, and it's relatively complex: PDF https://sel4.systems/Info/Docs/seL4-spec.pdf

The bottleneck seems to be that clearly it's critical to be certain about the spec.

Maybe not for kernels, but I can see use for cryptographic algorithms, etc?