[aorth]

There is automated static analysis from smatch for over ten years now:

https://lwn.net/Articles/691882/

This has found thousands of bugs in the kernel.