オペレーティングシステムカーネルの形式検証には、システムコールの意図された動作を正確に捉える仕様が必要である。これらの仕様を手動で記述するには深いドメイン専門知識が求められるため、大規模言語モデル（LLM）を用いてプロセスを自動化する動きが進んでいる。しかし、Hyperkernel OSカーネルから派生した245の仕様生成タスクからなるベンチマークOSV-Benchでは、これまで報告された最良のPass@1は55.10%に過ぎなかった。
このギャップを埋めるため、arXiv論文「BODHI: Precise OS Kernel Specification Inference」は、ドメイン知識プロンプティング手法であるBODHIを提案する。BODHIは、標準的なfew-shotプロンプトに、15カテゴリのドメイン固有翻訳パターンを網羅する構造化されたC-to-Python翻訳ガイドを追加する。構造化思考連鎖（SCoT）プロンプティングに触発され、このガイドは関心の分離の原則に従って翻訳を整理し、事前条件の抽出と事後条件の生成を別個のカテゴリとして扱う。
研究チームは、6社のプロバイダー（Anthropic、Mistral、Amazon、DeepSeek、Meta、Alibaba）からの9モデルでBODHIを評価した。これらのモデルは、 denseアーキテクチャ、mixture-of-expertsアーキテクチャ、推論アーキテクチャをカバーしている。結果として、BODHIはテストしたすべてのモデルを改善し、その向上幅は+11%から+32%に達した。最良の構成であるClaude Opus 4.6とBODHIの組み合わせは、96.73%のPass@1を達成し、以前報告された最良値を大きく上回った。
さらに、BODHIは構文エラーと意味エラーの両方を減少させ、構造化された参照資料を活用するのに十分な指示追従能力を持つモデルに対して最も強い効果を示した。これらの結果は、ドメイン知識の注入がモデル非依存の技術であり、汎用コード生成と形式仕様合成の間のギャップを大幅に埋めることを実証している。このアプローチは、OSカーネル形式検証の自動化に向けた有望な方向性を提供する。