3 ms·

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.

by Yoric 4y ago

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 4y ago
and how does it work? Do they write drivers in some verifiable subset of C?
- Yoric 4y ago
  That's how I understand it. I haven't checked the details.