BODHI：精确 OS 内核规范推断

对操作系统内核进行形式化验证需要捕捉系统调用预期行为的精确规范。手动编写这些规范需要深厚的领域专业知识，这促使使用大语言模型 (LLM) 自动化此过程。然而，在OSV-Bench这个来自 Hyperkernel OS 内核的 245 个规范生成任务基准中，最佳报告的 Pass@1 为 55.10%。我们提出一种域知识提示方法 (BODHI)，通过覆盖 15 类域特定转换模式的结构化 C 到 Python 转换指南来增强标准 few-shot 提示。受 Structured Chain-of-Thought (SCoT) 提示启发，该指南按关注点的分离对转换进行组织，分别处理 pre-condition 提取和 post-condition 生成。我们在来自 Anthropic、Mistral、Amazon、DeepSeek、Meta、Alibaba 六家提供商的九个模型（覆盖稠密、Mixture-of-Experts 和推理架构）上进行评估。BODHI 对每个测试的模型都提升了性能，提升幅度为 +11% 到 +32%。最佳配置 (Claude Opus 4.6 + BODHI) 达到 96.73% Pass@1。BODHI 减少了语法和语义错误，效果最明显的模型是那些拥有足够指令遵循能力以利用结构化参考材料的模型。这些结果表明，域知识注入是一种 model-agnostic 的技术，显著缩小了通用代码生成与形式规范合成之间的差距。