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

arXiv: https://arxiv.org/abs/2504.20964 · HTML: https://mlsanity.com/paper/2504.20964/

## Key facts

- Cited by 8 papers in the map (data through 14 Oct 2026).
- Builds on 23 of its 60 references that are in the map.
- First posted on arXiv 29 Apr 2025.

## Builds on (most cited first, 23 of 23)

- [Language Models are Few-Shot Learners](https://mlsanity.com/paper/2005.14165/) (2020)
- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [Program Synthesis with Large Language Models](https://mlsanity.com/paper/2108.07732/) (2021)
- [SWE-bench: Can Language Models Resolve Real-World GitHub Issues?](https://mlsanity.com/paper/2310.06770/) (2023)
- [WizardCoder: Empowering Code Large Language Models with Evol-Instruct](https://mlsanity.com/paper/2306.08568/) (2023)
- [A Survey on In-context Learning](https://mlsanity.com/paper/2301.00234/) (2022)
- [A Survey on Large Language Models for Code Generation](https://mlsanity.com/paper/2406.00515/) (2024)
- [Rethinking Benchmark and Contamination for Language Models with Rephrased Samples](https://mlsanity.com/paper/2311.04850/) (2023)
- [CrossCodeEval: A Diverse and Multilingual Benchmark for Cross-File Code Completion](https://mlsanity.com/paper/2310.11248/) (2023)
- [Multi-lingual Evaluation of Code Generation Models](https://mlsanity.com/paper/2210.14868/) (2022)
- [Large Language Models Meet NL2Code: A Survey](https://mlsanity.com/paper/2212.09420/) (2022)
- [InferFix: End-to-End Program Repair with LLMs](https://mlsanity.com/paper/2303.07263/) (2023)
- [IRIS: LLM-Assisted Static Analysis for Detecting Security Vulnerabilities](https://mlsanity.com/paper/2405.17238/) (2024)
- [Automatic Semantic Augmentation of Language Model Prompts (for Code Summarization)](https://mlsanity.com/paper/2304.06815/) (2023)
- [Clover: Closed-Loop Verifiable Code Generation](https://mlsanity.com/paper/2310.17807/) (2023)
- [Towards AI-Assisted Synthesis of Verified Dafny Methods](https://mlsanity.com/paper/2402.00247/) (2024)
- [DafnyBench: A Benchmark for Formal Software Verification](https://mlsanity.com/paper/2406.08467/) (2024)
- [Automated Proof Generation for Rust Code via Self-Evolution](https://mlsanity.com/paper/2410.15756/) (2024)
- [EquiBench: Benchmarking Large Language Models' Reasoning about Program Semantics via Equivalence Checking](https://mlsanity.com/paper/2502.12466/) (2025)
- [ComplexCodeEval: A Benchmark for Evaluating Large Code Models on More Complex Code](https://mlsanity.com/paper/2409.10280/) (2024)
- [CRUST-Bench: A Comprehensive Benchmark for C-to-safe-Rust Transpilation](https://mlsanity.com/paper/2504.15254/) (2025)
- [From Informal to Formal -- Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs](https://mlsanity.com/paper/2501.16207/) (2025)
- [Selene: Pioneering Automated Proof in Software Verification](https://mlsanity.com/paper/2401.07663/) (2024)

## Built on by (most cited first, 8 of 8)

- [ReflexiCoder: Teaching Large Language Models to Self-Reflect on Generated Code and Self-Correct It via Reinforcement Learning](https://mlsanity.com/paper/2603.05863/) (2026)
- [Agentic Specification Generator for Move Programs](https://mlsanity.com/paper/2509.24515/) (2025)
- [SysMoBench: Evaluating AI on Formally Modeling Complex Real-World Systems](https://mlsanity.com/paper/2509.23130/) (2025)
- [WebGen-R1: Incentivizing Large Language Models to Generate Functional and Aesthetic Websites with Reinforcement Learning](https://mlsanity.com/paper/2604.20398/) (2026)
- [TAROT: Test-driven and Capability-adaptive Curriculum Reinforcement Fine-tuning for Code Generation with Large Language Models](https://mlsanity.com/paper/2602.15449/) (2026)
- [CodePivot: Bootstrapping Multilingual Transpilation in LLMs via Reinforcement Learning without Parallel Corpora](https://mlsanity.com/paper/2604.18027/) (2026)
- [BODHI: Precise OS Kernel Specification Inference](https://mlsanity.com/paper/2605.23931/) (2026)
- [OSFoundry: Building and Evolving Operating Systems with Specification-Guided Agents](https://mlsanity.com/paper/2609.25018/) (2026)

## Abstract (arXiv)

We introduce OSVBench, a new benchmark for evaluating Large Language Models (LLMs) on the task of generating complete formal specifications for verifying the functional correctness of operating system kernels. This benchmark is built upon a real-world operating system kernel, Hyperkernel, and consists of 245 complex specification generation tasks in total, each of which is a long-context task of about 20k-30k tokens. The benchmark formulates the specification generation task as a program synthesis problem confined to a domain for specifying states and transitions. This formulation is provided to LLMs through a programming model. The LLMs must be able to understand the programming model and verification assumptions before delineating the correct search space for syntax and semantics and generating formal specifications. Guided by the operating system's high-level functional description, the LLMs are asked to generate a specification that fully describes all correct states and transitions for a potentially buggy code implementation of the operating system. Experimental results with 12 state-of-the-art LLMs indicate limited performance of existing LLMs on the specification generation task for operating system verification. Significant disparities in their performance highlight differences in their ability to handle long-context code generation tasks. The code are available at https://github.com/lishangyu-hkust/OSVBench