seL4 kernel was formally verified in 2014, what if all layers were verified? Shouldn't they be?

Pontifications

In Software is hard and won’t be what users want until there is security and real layers and components, I neglected to mention that in addition to security at all layers it would be even better if each base layer (ok maybe not apps but all layers below the app layer!) was formally verified as well as secure.
Just found out from Graydon about the micro-kernel seL4 which was verified in 2014.
What if the microcode was verified (i.e. the layers below the kernel)?
What if the upper layers were all verified (i.e. all the layers above the kernel except the application layer)?
What if this just wasn’t confined to military and banking software but was the norm; all layers below applications were verified and secure?
I think the software industry would be a lot less risky and bug prone if it were. And I don’t think it’s impossible and it just takes time and you only have to do it once (or a few times!).