[Yoric]

These days, Microsoft requires model-checking proofs before accepting new device drivers. That's their secret weapon that finally got (mostly) rid of the BSOD.

I suspect that Apple is also using model-checking at various layers, but I have no proof :)

[riku_iki]

and how does it work? Do they write drivers in some verifiable subset of C?

[Yoric]

That's how I understand it. I haven't checked the details.