Comment by ycombinatrix
9 days ago
They didn't "prove the kernel is correct", they built a tool to prove that a single driver maintains an invariant throughout execution.
9 days ago
They didn't "prove the kernel is correct", they built a tool to prove that a single driver maintains an invariant throughout execution.
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.