All non-trivial specs, like the one for seL4, are hard to verify. Lots of that complexity comes from interacting with the rest of the world which is a huge shared mutable global state you can't afford to ignore.

Of course, you can declare that the world itself is inherently sinful and imperfect, and is not ready for your beautiful theories but seriously.

it can tell you if your spec is bad, but it can't tell you if your spec is good