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.

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.