That's assuming the current models are able to find all the bugs, and that we won't have a better model out every few months that will be able to find even more obscure bugs.

We would also have to burn a trillion tokens a day verifying all the C code the hard way forever going forward. It would be cheaper to rewrite the kernel in Rust, subsystem and driver by driver at a time.