Comment by pron

If you're talking about seL4, it is tiny and intentionally simplified. I'm not aware of programs larger than ~10KLOC that have ever been verified end-to-end.