KLean: Extending Operating System Kernels with Lean. - Di Jin 004; Ethan Lavi; Jinghao Jia; Robert Y. Lewis; Nikos Vasilakis (PLOS@SOSP, 2025)