BODHI: Precise OS Kernel Specification Inference via Domain Knowledge Prompting

Forum topic · 小凯 · 2026-05-27

Summary

Formal verification of OS kernels requires precise specifications of system call behavior, but writing them manually demands deep domain expertise. BODHI is a domain knowledge prompting method that augments standard few-shot prompts with a structured C-to-Python translation guide covering 15 categories of domain-specific translation patterns. Inspired by Structured Chain-of-Thought (SCoT) prompting, it organizes translation by separation of concerns, treating pre-condition extraction and post-condition generation as distinct categories. On OSV-Bench, a benchmark of 245 specification generation tasks derived from the Hyperkernel OS kernel, BODHI improves all nine tested models from six providers (Anthropic, Mistral, Amazon, DeepSeek, Meta, Alibaba) across dense, mixture-of-experts, and reasoning architectures, with gains from +11% to +32%. The best configuration (Claude Opus 4.6 + BODHI) achieves 96.73% Pass@1 versus a previous best of 55.10%. The method reduces both syntax and semantic errors and works best on models with strong instruction-following ability, demonstrating that domain knowledge injection is a model-agnostic bridge between general code generation and formal specification synthesis.

Paper Overview

Field: ML Authors: Zhiming Chang, Ziyang Li Published: 2026-05-26 arXiv: 2505.21638

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%. 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.

Key Takeaways

Problem: LLMs struggle to generate precise kernel specifications; best prior Pass@1 on OSV-Bench was only 55.10%.
Method: BODHI adds a structured C-to-Python translation guide (15 pattern categories) to few-shot prompts, separating pre-condition extraction from post-condition generation.
Results: Improvements of +11% to +32% across nine models from six providers; top result of 96.73% Pass@1 with Claude Opus 4.6.
Insight: Domain knowledge injection is model-agnostic and most effective for models with strong instruction-following capability.

---

*Auto-collected on 2026-05-27*