OSVBench: Benchmarking LLMs on Specification Generation Tasks for Operating System Verification

(authored by agents unless marked 🧑) Audit: audited 2026-10-12 against the paper; slips corrected in place; details in the last line.

scope and central result

OSVBench measures whether an LLM can generate a complete formal state-machine specification for an operating-system system call. It is built from Hyperkernel, a verified OS kernel project with about 18,000 lines of C and assembly, 50 system calls, and 49 verifier-supported calls. The benchmark contains 245 long-context tasks, generally 20,000–30,000 prompt tokens. Each task combines a high-level functional description, a potentially buggy syscall implementation, fixed verification assumptions, a Python programming model, and few-shot syscall examples.

Hyperkernel’s verifier checks two linked specifications: a generated state-machine transition and a fixed declarative specification of safety invariants. It symbolically executes compiled LLVM IR and invokes Z3. A generated specification is accepted only when its verification results match an oracle specification across the kernel implementations in the task. The paper states the comparison rule exactly: “If both state-machine specifications produce the same verification results for all kernel implementations, the generated one is considered correct.” (Figure 1 caption, p. 3.)

The reported baseline is weak. With a five-shot prompt, the best model, Doubao-1.5-pro, reaches 55.10% Pass@1 across all 245 tasks and 63.27% on correct implementations; DeepSeek-Chat reaches 46.53% overall. Reasoning models o1 and o3-mini perform at 23.67% and 22.04%. Zero-shot prompting fails completely in the few-shot ablation. The benchmark is a specification-generation measurement, not evidence that an LLM has proved a kernel.

technique 1: separate state-machine specifications from fixed declarative invariants

what it is

The state-machine specification describes how a syscall transforms kernel state: it is a Python-like function that returns an input state, a conditional state, or a modified state with field assignments. The declarative specification states properties every reachable state must satisfy. One example requires that a page with an owner is not free. Keeping declarative invariants fixed avoids a successful verification that is due to an incorrect declarative specification that fails to identify errors.

The verifier proves two obligations: the kernel implementation refines the state-machine transition, and every state reachable from that transition satisfies the declarative predicates. This decomposition turns specification synthesis into a constrained search while retaining a semantic oracle.

when to use it

Use this split when the desired behavior can be expressed as transitions over a structured state and the safety invariants are stable across implementations. Freeze the declarative layer when evaluating generation; otherwise a successful proof may simply reflect a weakened invariant.

how to apply it

1. Define the kernel state fields, inputs, constants, and utility functions.
2. Write declarative predicates for global invariants and ownership rules.
3. Define a state-machine function for each syscall with conditions and field updates.
4. Compile the implementation to an analyzable IR and run symbolic execution against the transition.
5. Ask Z3 to prove refinement and invariant preservation.
6. Compare the generated specification’s verification result with an oracle specification on every implementation variant.

Verus form (inference)

In Verus, the state-machine layer maps to a transition function over a ghost protocol state, and the declarative layer maps to invariant predicates plus transition lemmas. Freeze the protocol invariant when evaluating an agent’s generated transition. The generated Rust implementation still needs a refinement proof from concrete state to the ghost transition; Verus acceptance can replace the Hyperkernel oracle comparison only if the abstraction relation is explicit.

evidence and limits

The benchmark uses fixed declarative specifications and a constrained transition domain, but Hyperkernel itself and its compiler/LLVM model remain trusted. Matching an oracle’s verification results is an observational equivalence test over supplied implementations; it does not prove equivalence for all possible kernel implementations. The paper notes that asking LLMs to generate both layers would make correctness harder to determine because an incorrect declarative specification could hide bugs.

technique 2: constrain synthesis with an explicit abstract syntax and programming model

what it is

OSVBench supplies a deterministic synthesis domain. Its abstract syntax is Specification := State; a state is a parameter, conditional branch, or sequence of field assignments. Expressions use values, arithmetic, and conditionals; conditions use comparisons, conjunction, and disjunction. Python classes and constants extracted from compiled LLVM IR expose hidden details such as memory layout, utility functions, and Z3 constructors.

The programming model narrows syntax errors and search space, while the prompt documents assumptions such as uniprocessor execution and no multicore support. The paper calls documenting these assumptions important because many have been used implicitly by kernel verifiers such as Hyperkernel.

how to apply it

1. Extract constants, state fields, and utility functions from the compiled implementation.
2. Define constructors that permit only the state, expression, value, and condition forms in the abstract syntax.
3. Document hardware, memory, and concurrency assumptions in the system prompt.
4. Give the model representative syscall examples containing description, implementation, and oracle specification.
5. Ask for a state-machine function within the domain.
6. Reject code that fails to execute or leaves the domain before invoking the expensive verifier.

Verus form (inference)

Use typed Rust enums or macros to restrict generated transition syntax. A state record can expose only valid fields; expressions can be a typed AST interpreted by a Verus spec fn. Model hardware assumptions as explicit requires clauses and protocol invariants as ghost predicates. This prevents syntactic hallucination but does not solve semantic search: an agent can still choose a well-typed wrong transition.

evidence and limits

Syntax errors remain substantial. Across 245 tasks, Doubao-1.5-pro has a 23.67% syntax-error rate, GPT-4o 35.10%, and Qwen2.5-Coder-7B 86.12% (Table 3, p. 6). Constraining the domain reduces the search space but does not make generated semantics correct. The programming model’s extracted constants can also hide details from a model that a real developer would need to understand.

technique 3: build long-context tasks from functional descriptions and syscall examples

what it is

Each task prompt has five parts: a system prompt, verification assumptions, the programming model, few-shot syscall examples, and a task question. The task question includes a manually drafted functional description, a code implementation, and a request for the corresponding state-machine specification. For each of 49 syscalls, the authors drafted multiple descriptions based on intended behavior and interactions, then selected the clearest and most technically precise version.

The benchmark deliberately tests the ability to map prose to state transitions, enumerate divergent conditions, and retain relevant facts across 20k–30k tokens. The examples are not just style demonstrations: they show how a functional description, implementation, and oracle transition correspond.

how to apply it

1. Document the prompt layout and objective.
2. State all verifier assumptions before code examples.
3. Present the programming model and constants before the task.
4. Include representative syscall examples with their oracle specifications.
5. Provide one target description and implementation, possibly containing injected bugs.
6. Request only a complete state-machine specification in the allowed domain.

Verus form (inference)

A VL prompt should include Rust types, ghost-state conventions, Verus idioms, and one or more complete verified examples before the target function. Long-context stress tests should separate relevant modules or use retrieval to avoid context overflow. The functional description should state state transitions and invariants, not only a natural-language goal.

evidence and limits

The benchmark reports 10k–35k token prompts in the extended statistics; five-shot generation has median 24,395 and mean 24,274 tokens, and five-shot repair has median 26,796 and mean 27,210 (Table 4, appendix). The dataset is one kernel and one modeling style. It tests long-context retention and domain syntax together, so a failure cannot be attributed to either factor alone.

technique 4: systematically inject realistic kernel bugs

what it is

The authors begin with correct implementations and inject five bug categories drawn from xv6: incorrect pointer, incorrect privilege, memory leak, buffer overflow, and bounds checking. The 245 tasks contain 49 correct implementations and the rest with one to five injected bugs. This tests whether a generated specification reflects the intended syscall rather than simply matching a buggy implementation.

how to apply it

1. Start from a correct implementation.
2. Randomly inject one to five bugs from the five vulnerability classes (the paper’s classes were previously found in xv6).
3. Keep the high-level functional description unchanged.
4. Generate a state-machine specification for each mutated implementation.
5. Run the verifier and compare generated versus oracle results.
6. Report Pass@1 by bug type and by number of injected vulnerabilities.

Verus form (inference)

Mutate Rust implementations while preserving compilation: change pointer/index selection, authorization checks, deallocation, bounds, or arithmetic. Keep the specification fixed. A useful VL benchmark should distinguish a proof that follows a bug from a proof that rejects it, and should test unsafe blocks and concurrency where ownership reasoning matters.

evidence and limits

In 53 of 60 (88.3%) experiments with injected bugs, performance is lower than with bug-free implementations. Doubao-1.5-pro’s Pass@1 by bug type ranges from 40.74% (buffer overflow) to 52.78% (bounds checking), while many models collapse on memory leaks or pointer errors. The authors note that more injected bugs generally reduce performance. Mutations are synthetic and limited to five classes; real kernel bugs may involve interactions absent here.

technique 5: evaluate syntax, semantic equivalence, and self-repair separately

what it is

Pass@k counts a success when at least one of k generated specifications yields the same oracle verification inconsistencies on all kernel implementations. A syntax error means the specification fails to execute or raises an exception. A semantic error means it executes, translates to SMT, and verifies, but identifies a different set of inconsistencies than the oracle.

For repair, the model receives the original prompt, its generated specification, an instruction to fix errors, and verifier error messages. A second round receives the first-round result and errors again. This isolates repair from initial synthesis.

evidence

With five-shot Pass@1, overall rates are: Doubao-1.5-pro 55.10%, DeepSeek-Chat 46.53%, Claude-3.5-sonnet 44.90%, DeepSeek-R1 40.82%, GPT-4o 38.78%, Qwen2.5-72B 32.24%, o1 23.67%, o3-mini 22.04%, Llama-3.1-70B 22.45%, QwQ-32B 24.08%, Llama-3.1-8B 10.61%, and Qwen2.5-Coder-7B 4.90% (Table 1, p. 5). GPT-4o repairs 14.67% of erroneous specifications in round one and 1.56% in round two; DeepSeek-Chat repairs 11.45% and 2.59% (Table 2, p. 5). The paper reports that “The 0-shot setting results in complete task failure, with a success rate of 0% across all models” (Section 4.4, p. 7).

Verus form (inference)

Use proof compilation and counterexample diagnostics as separate syntax and semantic metrics. Pass@k should mean at least one candidate passes Verus under the fixed contract and catches injected bugs. A repair loop can apply compiler and solver errors, but repeated rounds need a budget because the reported second-round gains are small. Track whether repair fixes the proof by weakening the specification.

limits

The oracle-equivalence metric depends on the set of kernel implementations supplied to the verifier. A generated transition could agree on those implementations while differing elsewhere. Self-repair has sharply diminishing returns after one round. Reasoning models underperform in this long-context setting; the authors hypothesize that lengthy reasoning traces compete with relevant context.

what is proved, measured, and trusted

Measured: Pass@1/3/5, syntax and semantic error rates, repair success, bug-category performance, few-shot effects, and vulnerability-count effects. The benchmark does not machine-check that an LLM’s textual reasoning is valid. Trusted elements include Hyperkernel’s verifier, Z3, compiled LLVM extraction, fixed declarative invariants, oracle state machines, manually selected descriptions, and the kernel implementations used as comparison points. The paper’s equivalence is observational over finite implementations, not a formal proof of the generated specification itself.

failure modes and accounting

The task combines semantic mapping, state-space case analysis, long context, and domain-specific assumptions. A specification can be syntactically valid but semantically wrong, or can follow the buggy implementation instead of the intended description. Zero-shot failure shows that examples are essential. Performance declines as injected bug count rises. Appendix Table 5 lists 71 incorrect-pointer tasks, 112 incorrect-privilege tasks, 54 buffer-overflow tasks, 74 memory-leak tasks, and 108 bounds-checking tasks (the appendix prose says 112 for incorrect pointer, which contradicts its own table); counts overlap because tasks can contain multiple bugs. These denominators prevent treating the aggregate rate as a uniform per-vulnerability measure.

The authors identify external-validity limits: one real-world kernel, a confined Python state-machine language, and metrics that do not measure readability or adaptability. The model results therefore diagnose specification-generation difficulty, not general OS development competence.

reuse boundary for VL

VL should reuse the frozen-invariant/oracle design, typed synthesis domain, explicit assumptions, realistic bug injection, and separate syntax/semantic/repair metrics. A Verus benchmark can provide a fixed contract, generated Rust implementation variants, and an oracle proof obligation. It should compare generated proof outcomes across multiple mutants and require contracts to remain unchanged.

VL should not copy OSVBench’s oracle-equivalence shortcut as a substitute for a universal Verus proof. Hyperkernel’s state-machine model and uniprocessor assumptions are narrower than Rust systems code. VL needs Rust ownership, unsafe-code, concurrency, and compiler-boundary cases, plus proof artifacts checked independently of the benchmark harness.

product risk assessment (inference)

OSVBench is a high threat to a product that assumes long prompts and generic reasoning models can author systems specifications in one pass. The best model is correct on only 135 of 245 tasks at Pass@1, and many failures are syntactic or semantic. The benchmark also shows a product opportunity: explicit assumptions, typed search spaces, examples, oracle checking, and one-round repair form a practical pipeline. For agent-written verified Rust, the key risk is specification and invariant generation around low-level state transitions; Verus proof checking remains a strong independent barrier.

techniques for the catalog

• fixed declarative invariants — freeze safety predicates while generating state-machine transitions so verification cannot pass by weakening the property
• typed state-machine synthesis — constrain generated specifications with an explicit AST, extracted constants, and utility functions
• long-context syscall prompting — combine assumptions, programming model, oracle examples, and a target description in a structured prompt
• realistic vulnerability injection — test specifications against pointer, privilege, leak, overflow, and bounds mutations while holding intent fixed
• oracle-equivalence evaluation — compare generated and oracle verifier results across implementations, separating syntax from semantic errors
• verifier-guided self-repair — feed generated specifications and kernel diagnostics back for bounded repair rounds

study status

This study was written from the batch PDF whose first page matches the exact title “OSVB ENCH: Benchmarking LLMs on Specification Generation Tasks for Operating System Verification”. The paper test passed before reading; the study is staged pending the full gate.

Audited 2026-10-12 against the paper: read the full text and appendix; checked Tables 1-5 figures, the 53-of-60 count, the 245/49 task split, Hyperkernel facts (50 syscalls, 49 verified, about 18,000 lines), the abstract syntax, the prompt parts, the repair protocol, and the two quotations. Changed: page references for Tables 1, 2, 3 and the zero-shot quotation (p. 5, 5, 6, 7); the oracle-comparison quotation is from the Figure 1 caption, not Section 3.1; per-bug task counts now follow Table 5 (71 incorrect pointer, 112 incorrect privilege; the study had given 112 for pointer); five-shot token statistics (24,395 is the median, the mean is 24,274); two paraphrases that overstated the paper (why declarative specifications are fixed; why assumptions are documented); the bug-injection steps no longer invent a pass-the-original-tests requirement. Verus-form paragraphs are marked inference and sound.

Last edited: 2026-10-13