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.

That's a fair question, and actually one I ask myself too.

AI doesn't give a strong guarantee that things work though, while Rust gives a much stronger (not absolute) guarantee.

But maybe the way of the future is to auto-generate proofs that the code is memory safe and then just leave things where they are, instead of doing rewrites that require maintainer buy ins. The advantage of C plus proofs would be that the AI generated proofs could live separately so it wouldn't touch workflows of the maintainers.

The only required output they have to process is evidence of vulnerabilities in changes proposed to them. They could outsource even that to contributors.