Drivers can crash the rest of the kernel in Windows 7. People playing games during the Windows 7 days should remember plenty of blue screens citing either graphics drivers (mainly for ATI/AMD graphics) or their kernel anticheat software. Second, a “proof of correctness” has never been made for any kernel. Even the seL4 guys do not call their proof a proof of correctness.
Kernel drivers have to be verified by the driver verifier to pass Windows Hardware Qualification Labs certification and get signed with the Windows signing key that lets them load without warnings. There are fewer outside kernel drivers today, though, because plugging random peripheral cards into PC buses is no longer a big thing.
This is true for certification, which is mandatory for Server OS, distributing through Windows Update, or certain classes of drivers such as anti-malware or biometric authentication, but you can still submit drivers to Microsoft for "attestation signing" that will load without warnings on desktop OS without having to run them through the testing suite.
In any case, running the certification tests does not provide runtime protection for drivers running in kernel mode, as demonstrated by CrowdStrike. Only Windows 10 started introducing hardware virtualization-based isolation of kernel components (to provide isolation of security subsystems, not runtime checks to prevent crashes): https://learn.microsoft.com/en-us/windows-hardware/design/de...
Yet drivers that have passed Windows Hardware Qualification Labs certification have had blue screens. Also, Microsoft hands out Windows kernel driver signing keys to anyone who pays them. You don't need to have a driver go through the Windows Hardware Qualification Labs to be able to sign it with a key signed by Microsoft.
It does not prove that the driver will not crash the kernel. It should be fairly easy to find a driver that passed QA testing under that tool, yet still crashed the kernel. You just need one of the many driver developers for Microsoft Windows to admit to having used that tool and fixed a crash bug that it missed, and you have an example. Likely all developers who have used that tool can confirm that they have had bugs that the tool missed.
