> А смысл в этом Runtime Verification?

Обнаружение некорректной работы системы в сюжетно интересных точках и довольно быстро.

> Упало ядро в панику в рантайме - значит всё плохо, вот вам и вся верификация.

Кроме этого есть вариант работать некорректно. Т.е. в случае каких-то сбоев, допустим, разрушения состояния RAM по той или иной причине (логической или физической) система может что-то делать, но совсем не так как было задумано.

Как простой пример, система может, например, повиснуть. Это и не паника, и не работа в задуманном виде. На этот случай в критичных системах есть вачдог. Но возможны и более сложные варианты, когда система как живая, но делает что-то явно не то. В этот момент ее глюкание лучше срубить: при панике это так или иначе будет подхвачено чем-то еще или просто failsafe, а если оно будет глюкать, оно может довольно долго и успешно ломать дров. А вот этого никому не надо. Это хозяйство рядом с RT_LINUX патчами продвигается, и интересно примерно тем же кому и эти патчи. Ну да, не вебмакакам и хомячкам на десктопе, и чего? Там и у RT_LINUX довольно странные требования при билдовке есть :)

> Если бы было можно взять и запилить эталонную модель, превратить ядро в детерминированную
> машину состояний, то это бы сделали, скомпилировали и получили идеальное ядро,
> но это слишком сложная задача, потому что ну нельзя для монолитного
> ядра предсказать все возможные состояния и переходы между ними.

Вон там предлагается сделать что-то наподобие, но для сюжетно интересного subset, и зайдя с совсем другого бока. А полную модель более-менее сложной системы отстроить нельзя - в чем факап и состоит. Однако сравнить трейс с эталонным в точках интереса для проверки что они пройдены верно это все совершенно не мешает.