[$] 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
run-time
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.