Technical Summary: BODHI: Precise OS Kernel Specification Inference

Problem Statement

The formal verification of operating system (OS) kernels is critical for safety-critical systems but is bottlenecked by the manual effort required to construct precise formal specifications. While Large Language Models (LLMs) have demonstrated proficiency in general code generation, their ability to synthesize formal specifications for OS kernels remains limited. The OSV-Bench benchmark, which evaluates the conversion of C system call implementations into Python/Z3 state-machine specifications, revealed a significant performance gap: the best reported Pass@1 score among 12 evaluated models was only 55.10%.

This gap stems from four primary challenges:

1. Long-context complexity: Prompts contain approximately 26K tokens, including programming models, examples, and target code.
2. Semantic gap: The task requires translating imperative C kernel code into declarative Z3 Python specifications, involving fundamentally different programming paradigms.
3. Interleaved concerns: C code often mixes pre-condition (error checking) and post-condition (state mutation) logic, which must be strictly separated in formal specifications.
4. Domain-specific knowledge: Kernel APIs involve specialized patterns (e.g., page table entry formulas, reference counting semantics, TLB flush operations) that are not covered by general-purpose LLM training.

Methodology: BODHI

The authors propose BODHI, a domain knowledge prompting method that augments standard few-shot prompts with a structured C-to-Python Translation Guide. Unlike standard Chain-of-Thought (CoT) or Structured Chain-of-Thought (SCoT) which focus on generating intermediate reasoning steps, BODHI injects structured reference material into the input context.

Prompt Structure

The BODHI prompt retains the four components of the OSV-Bench baseline:

1. System prompt (instructions).
2. Programming model (definitions of classes, constants, functions).
3. Five few-shot examples (C implementation to Z3 specification pairs).
4. Target task (functional description and C code).

BODHI adds a fifth component: a 519-line Translation Guide inserted between the few-shot examples and the target task. This placement leverages the "recency effect" in transformer attention, ensuring domain-specific patterns are most accessible during generation.

Translation Guide Design

The guide is organized into 15 categories derived from an iterative analysis of failures in a mid-tier model (Claude Haiku 4.5). It follows a Separation of Concerns principle, distinguishing between pre-condition extraction and post-condition generation. The categories are grouped into three tiers:

• Tier 1 (Syntax): Covers specification templates, pre-condition translation (negating C error checks), post-condition patterns, map field syntax (distinguishing read () vs. write []), operator rules, and constant prefixes.
• Tier 2 (Domain Semantics): Covers Page Table Entry (PTE) formulas (distinguishing x86 vs. IOMMU), shadow metadata, reference counting, TLB flush operations, state pointer names, and field name mapping.
• Tier 3 (Completeness): Addresses C helper function expansion, available helper inventories, and complex IPC state-machine patterns.

Crucially, the guide functions as a "domain textbook" containing general translation rules and illustrative patterns, not task-specific solutions or complete code.

Key Contributions

1. Domain-Specific Translation Guide: A structured 15-category guide covering C-to-Python/Z3 translation patterns derived from verified ground-truth specifications.
2. Comprehensive Evaluation: Testing across nine models from six providers (Anthropic, Mistral, Amazon, DeepSeek, Meta, Alibaba), covering dense, mixture-of-experts, and reasoning architectures.
3. Error Analysis: A detailed breakdown showing that BODHI reduces both syntax and semantic errors, with the most significant impact on mid-tier models that possess instruction-following capabilities but lack specific domain knowledge.
4. New State-of-the-Art: Achieving a Pass@1 of 96.73% on OSV-Bench, substantially exceeding the previous best of 55.10%.

Results

• Performance Gains: BODHI improved Pass@1 scores for every model tested, with gains ranging from +11.0% (Qwen3) to +31.8% (Devstral 2).
• Top Performance: The configuration of Claude Opus 4.6 + BODHI achieved 96.73%, failing on only 8 of 245 tasks.
• Error Reduction:
  • Syntax Errors: BODHI significantly reduced syntax errors, particularly type/sort mismatches and API misuse (e.g., using parentheses for map writes). For Devstral 2, syntax errors dropped from 31.0% to 8.2%.
  • Semantic Errors: The guide effectively addressed domain pattern errors (e.g., incorrect PTE formulas) and translation logic errors. For Claude Opus 4.6, baseline failures were almost exclusively domain pattern errors; BODHI reduced these to 2.4%.
• Model Agnosticism: The improvements were consistent across diverse architectures and providers, suggesting the technique is not tied to a specific model family's training data.
• Mid-Tier Optimization: The largest relative gains were observed in mid-tier models (e.g., Devstral 2, Claude Haiku 4.5), which have sufficient instruction-following ability to utilize the guide but lack the intrinsic domain knowledge of top-tier models.

Significance and Claims

The paper claims that domain knowledge injection is a model-agnostic technique that effectively bridges the gap between general-purpose code generation and formal specification synthesis. The authors argue that the bottleneck in OS kernel verification is not the LLM's reasoning capability (as reasoning-optimized models like o1 and DeepSeek-R1 did not outperform standard instruction-following models) but rather the lack of specific translation knowledge.

By structuring domain knowledge into a reference guide rather than relying on few-shot examples alone, BODHI enables LLMs to correctly handle complex kernel semantics such as page table formulas and reference counting. The work demonstrates that a productive division of labor exists where human experts construct the domain guide, and LLMs apply it at scale to achieve near-perfect specification synthesis. The authors note that the approach is limited by the cost of guide construction and the model's ability to adhere to output formats, but it offers a reproducible path to improving formal verification without model retraining.