The frequent tweaking of heuristics in the Linux kernel task scheduler suggests a need for formal verification, to ensure that important properties are maintained. Nevertheless, writing and verifying specifications for Linux kernel code have been considered to be impractical, leading other operating system verification efforts to propose co-design of new code and associated specifications instead. Furthermore, the Linux kernel evolves frequently, making any verification effort quickly out of date. Still, verification tools for C code are becoming more and more robust. In this paper, we explore whether it is now possible to apply formal verification directly to Linux kernel code, and to maintain the resulting specifications as the Linux kernel evolves. Our experiment focuses on the function should_we_balance, which is the gatekeeper to the Linux kernel scheduler’s load balancer, and on the verification tool Frama-C.