[$] Extending run-time verification for the kernel
There are a lot of things people expect the Linux kernel to do correctly. Some
of these are checked by testing or static analysis; a few are ensured by
run-time verification: checking a live property of a running Linux system. For
example, the scheduler has a handful of different correctness properties that
can be
checked in this way.
Nam Cao posted a
patch series that aims to extend the kinds of properties that the kernel's
verification system can check, by adding support for
linear temporal logic (LTL). The patch set has seen eleven revisions since the
first version in March 2025, and recently made it into the linux-next
tree, from where it seems likely to reach the mainline kernel soon.