Здравствуйте, Aleх, Вы писали:

A>Некоторые (не помню кто) на этом форуме считают, что и x86 код можно верифицировать, но это не правда.

Можно верифицировать жестко ограниченное подмножество x86 кода и это уже сделано например тут
http://code.google.com/p/native-nt-toolkit/ но боюсь драйверы на таком подмножестве тоже не особо попишешь.