# BODHI: Precise OS Kernel Specification Inference

arXiv: https://arxiv.org/abs/2605.23931 · HTML: https://mlsanity.com/paper/2605.23931/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 16 of its 23 references that are in the map.
- First posted on arXiv 22 Apr 2026.

## Builds on (most cited first, 16 of 16)

- [Chain-of-Thought Prompting Elicits Reasoning in Large Language Models](https://mlsanity.com/paper/2201.11903/) (2022)
- [Retrieval-Augmented Generation for Knowledge-Intensive NLP Tasks](https://mlsanity.com/paper/2005.11401/) (2020)
- [Program Synthesis with Large Language Models](https://mlsanity.com/paper/2108.07732/) (2021)
- [Lost in the Middle: How Language Models Use Long Contexts](https://mlsanity.com/paper/2307.03172/) (2023)
- [A Survey on Large Language Models for Code Generation](https://mlsanity.com/paper/2406.00515/) (2024)
- [Structured Chain-of-Thought Prompting for Code Generation](https://mlsanity.com/paper/2305.06599/) (2023)
- [Baldur: Whole-Proof Generation and Repair with Large Language Models](https://mlsanity.com/paper/2303.04910/) (2023)
- [IRIS: LLM-Assisted Static Analysis for Detecting Security Vulnerabilities](https://mlsanity.com/paper/2405.17238/) (2024)
- [Scallop: A Language for Neurosymbolic Programming](https://mlsanity.com/paper/2304.04812/) (2023)
- [SpecGen: Automated Generation of Formal Program Specifications via Large Language Models](https://mlsanity.com/paper/2401.08807/) (2024)
- [When LLMs Meet API Documentation: Can Retrieval Augmentation Aid Code Generation Just as It Helps Developers?](https://mlsanity.com/paper/2503.15231/) (2025)
- [Locus: Agentic Predicate Synthesis for Directed Fuzzing](https://mlsanity.com/paper/2508.21302/) (2025)
- [OSVBench: Benchmarking LLMs on Specification Generation Tasks for Operating System Verification](https://mlsanity.com/paper/2504.20964/) (2025)
- [Relational Programming with Foundation Models](https://mlsanity.com/paper/2412.14515/) (2024)
- [QLCoder: A Query Synthesizer For Static Analysis of Security Vulnerabilities](https://mlsanity.com/paper/2511.08462/) (2025)
- [Lobster: A GPU-Accelerated Framework for Neurosymbolic Programming](https://mlsanity.com/paper/2503.21937/) (2025)

## Abstract (arXiv)

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%. We propose a domain knowledge prompting method (BODHI), which augments the standard few-shot prompt with a structured C-to-Python translation guide covering 15 categories of domain-specific translation patterns. Inspired by Structured Chain-of-Thought (SCoT) prompting, the guide organizes translation by separation of concerns, addressing pre-condition extraction and post-condition generation as distinct categories. Evaluated on nine models from six providers (Anthropic, Mistral, Amazon, DeepSeek, Meta, Alibaba), covering dense, mixture-of-experts and reasoning architectures, BODHI improves every model tested, with gains ranging from +11% to +32%. The best configuration (Claude Opus 4.6 + BODHI) reaches 96.73% Pass@1. BODHI reduces both syntax and semantic errors, with the strongest effect on models that have sufficient instruction-following capability to utilize structured reference material. These results demonstrate that domain knowledge injection is a model-agnostic technique that substantially bridges the gap between general-purpose code generation and formal specification synthesis.