The article is extremely shallow beyond saying "Formal verification a la SPARK" should have been used, while not offering how this could actually work in the real world - I don't think the author has any experience working on any similar piece of software either.

While such techniques are available, would they be really applicable in a very dynamic environment such as with millions of PCs running various windows versions, needing continuous / real-time updates.

And yes, we of course know that QA and testing magically removes all possible failure modes/bugs.

> While such techniques are available, would they be really applicable in a very dynamic environment such as with millions of PCs running various windows versions, needing continuous / real-time updates.

I don't see much difference in complexity between the affected software and the several existing formally verified software. At the very least the parser/interpreter could very much be formally verified.

But my point is, have they tried? They don't seem to be even aware of such.

The industry doesn't want to pay what it costs to support the type of SDETs capable of doing QA on kernel drivers. Anyone that talented is going to do the math and switch to being a developer for a much bigger paycheck instead.