[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.