BODHI：精确的操作系统内核规约推断

操作系统内核的形式化验证需要能够刻画系统调用预期行为的精确规约。人工编写这些规约需要深厚的领域专业知识，这促使人们借助大语言模型（LLM）将该过程自动化。然而，在OSV-Bench——一个由Hyperkernel操作系统内核衍生出的245个规约生成任务组成的基准——上，已报道的最佳Pass@1为55.10%。我们提出一种领域知识提示方法（BODHI），它在标准少样本提示的基础上增补一份结构化的C到Python翻译指南，涵盖15类领域特定的翻译模式。受结构化思维链（SCoT）提示的启发，该指南按关注点分离来组织翻译，将前置条件提取与后置条件生成作为不同的类别加以处理。我们在来自六家提供商（Anthropic、Mistral、Amazon、DeepSeek、Meta、阿里巴巴）的九个模型上进行评估，涵盖稠密、混合专家与推理架构，BODHI提升了所有受测模型，增益介于+11%至+32%。最佳配置（Claude Opus 4.6 + BODHI）达到96.73%的Pass@1。BODHI同时减少语法与语义错误，对那些具备足够指令遵循能力以利用结构化参考资料的模型效果最强。这些结果表明，领域知识注入是一种模型无关的技术，能够实质性地弥合通用代码生成与形式化规约合成之间的差距。