Re: [PATCH 0/9] Kernel API Specification Framework

[Dmitry Vyukov]

On Sat, 14 Mar 2026 at 19:18, Jakub Kicinski <ku...@kernel.org> wrote:
>
> On Fri, 13 Mar 2026 11:09:10 -0400 Sasha Levin wrote:
> > This enables static analysis tools to verify userspace API usage at compile
> > time, test generation based on formal specifications, consistent error handling
> > validation, automated documentation generation, and formal verification of
> > kernel interfaces.
>
> Could you give some examples? We have machine readable descriptions for
> Netlink interfaces, we approached syzbot folks and they did not really
> seem to care for those.

I think our reasoning wrt syzkaller was that not all interfaces in all
relevant kernels are described with netlink yml descriptions, so we
need to continue using the extraction of interfaces from the source
code. And if we have that code, then using yml as an additional data
source only adds code/complexity. Additionally, we may extract some
extra constraints/info from code that are not present in yml.

Realistically system call descriptions may have the same problem for
us at this point, since we extract lots of info from the source code
already:
https://raw.githubusercontent.com/google/syzkaller/refs/heads/master/sys/linux/auto.txt
(and LLMs obviously can allow us to extract more)

[Jakub Kicinski]

yup! we haven't tried to make the yml spec super useful to syzbot
to be fair. I'm just flagging that example because in our case we
quickly went from "this will obviously be useful to syzbot" to
"although we could, it may not be super practical"

> (and LLMs obviously can allow us to extract more)

Didn't even think of that. LLMs should make short work of this sort of
extraction of information from source code..

[Sasha Levin]

On Mon, Mar 16, 2026 at 03:57:56PM -0700, Jakub Kicinski wrote:
>Didn't even think of that. LLMs should make short work of this sort of
>extraction of information from source code..

This is the primary reason that this proposal resurfaced :)

I've originally proposed[1] something like this almost a decade ago, but when I
started trying to write the actual specs I hit a brick wall: it was simply not
tractable.

With LLMs, writing the specs is something we can actually pull off, and we can
verify their correctness so LLMs don't get to hallucinate.

The specs you see in the following patches are all LLM generated.

--
Thanks,
Sasha