arXiv cs.AITuesday · May 26, 2026FREE

BODHI: Precise OS Kernel Specification Inference

Researchers propose BODHI (domain knowledge prompting) to automate formal specification generation for OS kernels. The method augments standard few-shot prompts with a structured C-to-Python translation guide covering 15 categories of domain-specific patterns, inspired by Structured Chain-of-Thought (SCoT) prompting. It separates pre-condition extraction and post-condition generation. Evaluated on nine models from Anthropic, Mistral, Amazon, DeepSeek, Meta, and Alibaba—including dense, mixture-of-experts, and reasoning architectures—BODHI improves every model by +11% to +32%. The best configuration (Claude Opus 4.6 + BODHI) reaches 96.73% Pass@1 on OSV-Bench, a benchmark of 245 specification tasks from the Hyperkernel OS kernel, compared to the previous best of 55.10%. The paper is available on arXiv.