Подожди. Ты замахнулся слишком далеко. Например, есть модуль ядра, который написан таким образом, что ввергает ядро в панику. Да, это ошибка автора модуля. Но вместе с тем формально, паника в данном случае является корректным поведением системы. Которое будет отображено в модели именно таким образом.
Соответсвенно, вопрос - от чего этот верификатор корректности защищает критически важные системы? Ну, то есть это очередной оверхед, чтобы подлизнуть безопасникам: полезной работы он не выполняет, но грузит системы довольно ощутимо. И как написано в статье - этот механизм предлагается навешивать на критически важные системы в довесок к тому "безопасному" маразму, который там уже есть. Ну и когда система будет заниматься полезной работой? она же при таком подходе занята исключительно проверками корректности и "безопасности" своей работы.