[$] Extending run-time verification for the kernel
There are a lot of things people expect the Linux kernel to do correctly. Someof these are checked by testing or static analysis; a few are ensured byrun-time verification: checking a live property of a running Linux system. Forexample, the scheduler has a handful of different correctness properties thatcan bechecked in this way.Nam Cao posted apatch series that aims to extend the kinds of properties that the kernel'srun-timeverification system can check, by adding support forlinear temporal logic (LTL). The patch set has seen eleven revisions since thefirst version in March2025, and recently made it into the linux-nexttree, from where it seems likely to reach the mainline kernel soon.