Sharpen the Spec, Cut the Code: A Case for Generative File System with SYSSPEC
Qingyuan Liu, Mo Zou, Hengbin Zhang, Dong Du, Yubin Xia, Haibo Chen
Abstract
File systems are critical OS components that require constant evolution to support new hardware and emerging application needs. However, the traditional paradigm of developing features, fixing bugs, and maintaining the system incurs significant overhead, especially as systems grow in complexity. This paper proposes a new paradigm, generative file systems, which leverages Large Language Models (LLMs) to generate and evolve a file system from prompts, effectively addressing the need for robust evolution. Despite the widespread success of LLMs in code generation, attempts to create a functional file system have thus far been unsuccessful, mainly due to the ambiguity of natural language prompts. This paper introduces SYSSPEC, a framework for developing generative file systems. Its key insight is to replace ambiguous natural language with principles adapted from formal methods. Instead of imprecise prompts, SYSSPEC employs a multi-part specification that accurately describes a file system's functionality, modularity, and concurrency. The specification acts as an unambiguous blueprint, guiding LLMs to generate expected code flexibly. To manage evolution, we develop a DAG-structured patch that operates on the specification itself, enabling new features to be added without violating existing invariants. Moreover, the SYSSPEC toolchain features a set of LLM-based agents with mechanisms to mitigate hallucination during construction and evolution. We demonstrate our approach by generating SPECFS, a concurrent file system. SPECFS demonstrates equivalent level of correctness to that of a manually-coded baseline across hundreds of regression tests. We further confirm its evolvability by seamlessly integrating 10 real-world features from Ext4. Our work shows that a specification-guided approach makes generating and evolving complex systems not only feasible but also highly effective.
Ask about this paper
Your agent reads all of it.
Lune indexed this paper to the last equation, along with the top-tier papers that cite it. Ask a question and the answer quotes them.
Builds on16
- AutoCodeRover: Autonomous Program ImprovementYuntong Zhang, Haifeng Ruan, Zhiyu Fan, Abhik RoychoudhuryISSTA 2024 · 96 citations
- CodeT: Code Generation with Generated TestsBei Chen, Fengji Zhang, Anh Nguyen, Daoguang Zan et al.ICLR 2023 · 64 citations
- Anvil: Verifying Liveness of Cluster Management ControllersXudong Sun, Wenjie Ma, Jiawei Tyler Gu, Zicheng Ma et al.OSDI 2024 · 50 citations
- SpecGen: Automated Generation of Formal Program Specifications via Large Language ModelsLezhi Ma, Shangqing Liu, Yi Li, Xiaofei Xie et al.ICSE 2025 · 25 citations
- API-Driven Program Synthesis for Testing Static Typing ImplementationsThodoris Sotiropoulos, Stefanos Chaliasos, Zhendong SuPOPL 2024 · 15 citations
Related papers
- From Commands to Prompts: LLM-based Semantic File System for AIOSZeru Shi, Kai Mei, Mingyu Jin, Yongye Su et al.ICLR 2025
- OSVBench: Benchmarking LLMs on Specification Generation Tasks for Operating System VerificationShangyu Li, Juyong Jiang, Tiancheng Zhao, Jiasi ShenAAAI 2026 · 10 citations
- SpecAgent: A Speculative Retrieval and Forecasting Agent for Code CompletionGeorge Ma, Anurag Koul, Qi Chen, Yawen Wu et al.ACL 2026 · 3 citations
- Automated Repair of Ambiguous Problem Descriptions for LLM-Based Code GenerationHaoxiang Jia, Robbie Morris, He Ye, Federica Sarro et al.ASE 2025 · 6 citations
- SpecMind: Cognitively Inspired, Interactive Multi-Turn Framework for Postcondition InferenceCuong Chi Le, Minh V. T. Pham, Tung Duy Vu, Cuong Duc Van et al.ACL 2026 · 2 citations
