honestly LLMs could probably write drivers in CompCert C or some other formally verified dialect. having AI discharge proof obligations seems like a terrific use for all this newly-developed mathematical process.

you could have the driver code prove it implements a spec, that there's no UB, that hardware invariants are maintained, that routines take a fixed time to execute.

the formal driver spec must still be written by sober, well-caffeinated humans of course.