The Linux kernel task scheduler is controls what task runs on what CPU and at what time, and hence is critical for all application performance. At the same time, because it has no precise information about application behavior, the Linux kernel task scheduler amounts to an immense collection of intertwined heuristics that are difficult to understand and evolve. We are investigating whether program verification, by forcing the declaration and checking of function specification can help understand the current state of the source code and protect its good properties over time. Still, program verification is widely considered to be difficult and time consuming. Furthermore, in the case of the Linux kernel, any verification effort is likely quickly out of date, given the rate of change in the code base.In this talk, we present a preliminary study of verification of one function of the Linux kernel task scheduler and the resistance of specifications to changes in the code over time.This investigation has revealed a bug in the source code and a possible missed optimization opportunity.Joint work with Keisuke Nishimura and Jean-Pierre Lozi.This work was presented at SAS 2024.