BODHI: Precise OS Kernel Specification Inference via Domain Knowledge Prompting

Forum topic · 小凯 · 2026-05-27

Summary

Formal verification of OS kernels requires precise syscall behavior specifications, but writing them manually demands deep domain expertise. BODHI is a domain knowledge prompting method that augments standard few-shot LLM prompting 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 separates concerns by treating pre-condition extraction and post-condition generation as distinct categories. Evaluated on nine models from six providers (Anthropic, Mistral, Amazon, DeepSeek, Meta, Alibaba), spanning dense, mixture-of-experts, and reasoning architectures, BODHI improves every tested model with gains from +11% to +32% on OSV-Bench, a benchmark of 245 specification generation tasks derived from the Hyperkernel OS kernel. The best configuration (Claude Opus 4.6 + BODHI) reaches 96.73% Pass@1, compared to a previous best of 55.10%. The method reduces both syntax and semantic errors, working best on models with strong instruction-following ability, demonstrating that domain knowledge injection is a model-agnostic technique bridging 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

BODHI injects domain knowledge into LLM prompts via a structured C-to-Python translation guide with 15 categories of translation patterns.
The method follows SCoT-style separation of concerns: pre-condition extraction and post-condition generation are handled as distinct steps.
On OSV-Bench (245 tasks from the Hyperkernel kernel), BODHI improves all nine tested models by +11% to +32%.
Best result: 96.73% Pass@1 with Claude Opus 4.6 + BODHI, up from a prior best of 55.10%.
Gains are strongest for models with sufficient instruction-following capability, suggesting domain knowledge injection is broadly applicable.

---

*Auto-collected on 2026-05-27*