If you're interested, the German Verisoft project [1] aims at such pervasive verification. AFAIK they haven't yet verified anything matching the complexity of seL4, but they did verify a simple real-time OS. Of course you do need to stop somewhere, as in trusting something "blindly" (say, the verification tools themselves and the hardware they run on).

[1] http://www.ertos.nicta.com.au/publications/papers/Klein_08.p...