News for hackers. Stuff that matters.

A comment on Windows 2000 Server named peak Microsoft. Readers say all downhill since Clippy. Parent comment

Re:Windows 2000 Server named peak Microsoft. Readers say all... by ycombinatrix on Saturday April 12, 2025 @12:34AM (#43661374)
They didn't "prove the kernel is correct", they built a tool to prove that a single driver maintains an invariant throughout execution.
[ Parent | on HN ]
Re:Windows 2000 Server named peak Microsoft. Readers say all... by ryao on Monday April 14, 2025 @03:14AM (#43678834)
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.
[ Parent | on HN ]