Subj : [$] Extending run-time verification for the kernel
To   : All
From : LWN.net
Date : Thu Jul 31 2025 06:40:08



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.

https://lwn.net/Articles/1030685/
--- SBBSecho 3.29-Linux
 * Origin: Palantir * palantirbbs.ddns.net * Pensacola, FL * (86:200/23)

.