It's going to take me a while to fully understand this paper. I wonder what the route to incorporating something like this in the Linux kernel would look like?
Generating readable C code was an important goal from early on. Parts of the linux kernel would have to be translated to Low*, which is the subset of F*, that can be extracted to C.
I guess there would be a new build step, that runs when code is checked in, to not burden everyone with all the new toolchain (F*, z3, karamel, maybe OCaml and more). While the generated C code can be read and understood by C programmers, changes to that part should be done in Low* and that may require changes to proofs in F* or to the extraction tool (karamel). That's a pretty big investment for a project like linux and I guess, any work in that direction will happen on forks for a while, before there is enough confidence that such changes are sustainable.
A good first candidate may be HACL* (https://hacl-star.github.io), a cryptographic library that is already used in several projects.
The end result is generated C code. So you could simply add the generated C code to the kernel like you would any other C code. And keep the proof chain separate from the kernel. My guess is that it is what Microsoft is doing with the kernel code.
My question was more around that it would have to replace existing code, so you'd need to advocate for it and come up with some way of incorporating it in the build. I'm not all that familiar with the development culture of the kernel but I imagine that large changes like this would have to be introduced slowly
