Nature of Quality
I specialize not in getting code right, but in getting design right.
seL4 does so well not because they proved compliance with specs, but because those specs were very good.
The serious flaws are in bad design, not bad code.
You can fix the code.
It is often impossible to fix bad design.
The machine code that seL4 proved to be compliant was small and this was possible because of good design.
The application security and integrity depended mainly on this small proven code.
I am sure that the proof helped avoid bugs.
(It would help if more people could understand those specs in native form.)
Few programmers can wrap their heads around the idea that security in a cap system does not rely on keeping bad code off the system.
With good design, and a small amount of correct code, you can achieve security and integrity despite the luxury of massive code on your system.
For integrity all code called upon by the application must be correct.
For security an even smaller subset at “the boundary” must be correct.