Hi Hanno, Just to add to what Eric said...
On Sat, Nov 29, 2025 at 04:19:11PM -0800, Eric Biggers wrote: > I think you may be underestimating how much the requirements of the > kernel differ from userspace. Consider the following: I've added a bit of formally verified code to the kernel, and also ported some userspace crypto. In these cases, I wound up working with the authors of the code to make it more suitable to the requirements of kernel space -- even down to the formatting level. For example, the HACL* project needed some changes to KReMLin to make the variety of code fit into what the kernel expected. Andy Polyakov's code needed some internal functions exposed so that the kernel could do cpu capability based dispatch. And so on and so forth. There's always _something_. I'd love to have a formally verified ML-DSA implementation (if we're to have ML-DSA in the kernel anyhow, but it looks like that's happening). But I almost guarantee that it's going to be some work to do. If those are efforts you'd consider undertaking seriously, I'd be happy to assist or help guide the considerations. There's also another approach, which would be to formally verify Eric's code, perhaps even using the same techniques as your own project, via CBMC and such. In this case, the name of the game is usually to port the kernel code to userspace. That generally winds up being a matter of shimming out some headers and adding a few typedefs. There's a decent amount of kernel test code or kernel tool code that does this, and lots of shim headers already in the kernel that can be borrowed for this. But usually, at least for crypto code, you can figure it out pretty quickly by just trying to compile it and plugging the missing headers and types as they come up. The model checking might be more work with this latter approach, since it's not already done like it is for the former, but the porting work is probably much less arduous. Anyway, the bigger picture is that I'm very enthusiastic about getting formally verified crypto in the kernel, so these types of efforts are really very appreciated and welcomed. But it just takes a bit more work than usual. Jason
