Je suis partiellement d'accord avec Godzil : un bootloader ou un micro-noyau, ça n'est pas forcément beaucoup de code, en tout cas bien moins qu'un navigateur ou une base de donnée et intrinsèquement ça n'est pas terriblement complexe. On a même des micro-noyaux comme SeL4 qui on été formellement prouvés.
Maintenant je suis aussi d'accord avec Zerosquare : même si le code n'est pas toujours intrinsèquement complexe, la vérification reste quelque-chose de difficile. Il y a de nombreuses subtilité de programmation, notamment avec le C et ses undefined behavior à tous les étages. Ça reste envisageable d'essayer de cacher une faille. Et puis au niveau des OS on a généralement plutôt des noyau massif qui même s'ils ne sont pas forcément complexe a comprendre, sont assez massif pour qu'ils soient dur à vérifier.