Sharpen the Spec, Cut the Code: A Case for Generative File System with SYSSPEC
summary
Claims a working pipeline that uses SYSSPEC to generate a concurrent file system called SPECFS from high-level formal-style specs, producing ~4,000 lines of C and integrating 10 Ext4 features while matching a manual baseline on hundreds of regression tests. The toolchain uses a spec compiler + validator feedback loop (about 30% of modules need at least one retry) and a DAG-structured SpecPatch with rely/guarantee nodes to add features without breaking existing invariants. LLM agents and modular specs handle concurrency and composition.
AI-written summary · about
chapters (9)
- 0:00Generative file systems intro
- 2:04LLMs for file systems
- 3:26Generative FS challenges
- 6:14SysFS spec design
- 9:42Concurrency in SysFS specs
- 10:45SpecPatch for evolution
- 11:51C-spec tool chain
- 13:13SpecFS case study
- 15:22Conclusion
related talks
14mBreaking the Reward Barrier: Accelerating Tree-of-Thought Reasoning via Speculative...
22mTowards Automated Verification of LLM-Synthesized C Programs
33mCorrectness Too Cheap To Meter: Formal Verification and LLMs
23mUsing LLM Generated Formal Specs to Prevent the Next DeFi Hack
48mSpec Driven Modernization: Spec2Cloud & GHCP Modern CLI
12mBuild bravely: Delivering risky projects
38mAutomatically Synthesising Programs that We Can Trust
22mStop pedaling: First principles for spec-driven agentic development