[ryao]

Any kind of modularity will result in people treating modules as black boxes, even when they are not. If you use a monokernel/hybrid that is OSS, then there might be plenty of code and you might treat it as a black box, but it is not a black box. If you use a microkernel, then the amount of code is likely even less. Microkernels exist that are formally verified and while unikernels cannot be formally verified without formally verifying the application that is a part of them. Formally verifying an application would be awesome, but few would ever do that.