BODHI: Precise OS Kernel Specification Inference
The paper titled 'BODHI: Precise OS Kernel Specification Inference' introduces a method to enhance the formal verification of operating system kernels. This method utilizes large language models to automate the generation of precise specifications, achieving significant improvements in performance. The results indicate that domain knowledge injection can effectively bridge the gap between general-purpose code generation and formal specification synthesis.
- ▪The best reported Pass@1 for specification generation tasks is 55.10%.
- ▪BODHI improves every model tested, with performance gains ranging from +11% to +32%.
- ▪The best configuration reaches a Pass@1 of 96.73%.
Opening excerpt (first ~120 words) tap to expand
Computer Science > Artificial Intelligence arXiv:2605.23931 (cs) [Submitted on 22 Apr 2026] Title:BODHI: Precise OS Kernel Specification Inference Authors:Zhiming Chang, Ziyang Li View a PDF of the paper titled BODHI: Precise OS Kernel Specification Inference, by Zhiming Chang and 1 other authors View PDF HTML (experimental) Abstract:The formal verification of operating system kernels requires precise specifications that capture the intended behavior of system calls. Writing these specifications manually demands deep domain expertise, motivating the use of large language models (LLMs) to automate the process. However, in OSV-Bench, a benchmark of 245 specification generation tasks derived from the Hyperkernel OS kernel, the best reported Pass@1 is 55.10%.
…
Excerpt limited to ~120 words for fair-use compliance. The full article is at arXiv cs.AI.
Discussion
0 commentsMore from arXiv cs.AI
