I think 6) is a very good point. The simple reaction to it is, well, I just define a small verification kernel that I trust, and the rest is just scaffolding that does not need to be trusted in order to have full confidence in the verification. Of course, that is not really true, because how do you know that the data arrives properly at the kernel, and is properly read off the kernel? In practice though, the small verification kernel idea works very well. I don't think that this is the final stage of how these systems are designed, though. I think we need to model the full system inside the system, and verify it this way. We can trust this verification because we are verifying it with a system with a small verification kernel, but afterwards, we can replace the small kernel with the modules we have proven to be correct now.