SL-VC: A Benchmark and Automated Framework for Separation Logic Verification Condition Proving

Formal verification of system software with complex heap manipulations remains challenging. Standard automated solvers frequently fail to discharge separation logic verification conditions even when correct specifications like loop invariants are provided, forcing verification engineers to manually construct proofs. While large language models (LLMs) have shown promise in proof synthesis, specialized approaches for separation logic remain unexplored. To bridge this gap, we introduce SL-VC (Separation Logic Verification Conditions), a benchmark of 289 verification conditions from textbook implementations of data structures and algorithms together with real-world C code, including the LiteOS kernel's linked list library and the mini-gmp library. Our evaluation reveals that general-purpose LLMs and existing LLM-based Rocq provers struggle to effectively discharge these verification conditions. To address this challenge, we propose SPLIT (Split spatial and pure Proving with LLM-frIendly Tactics), a novel framework that enables predictable proof state transitions through an LLM-friendly tactic library, combined with a two-stage workflow that separates spatial and pure reasoning to align with separation logic semantics. Experimental results on SL-VC demonstrate that SPLIT consistently outperforms existing approaches, showing that LLM-assisted proof synthesis is a promising solution for separation logic verification of real-world system software.

Modern systems software often changes complicated data structures in memory, such as linked lists, trees, and arrays. Formal verification tries to prove that such software behaves correctly, but the proof tasks produced by verification tools can be very hard to solve automatically. As a result, human experts often have to guide these proofs by hand, which makes verification slow and difficult to scale. We study whether large language models can help with this missing proof step. We introduce SL-VC, a benchmark of 289 proof tasks drawn from textbook data-structure programs and real C code, including parts of LiteOS and mini-gmp. We also build SPLIT, a workflow that uses language-model-friendly proof commands and breaks each proof into clearer steps: first reasoning about the layout of memory, then reasoning about ordinary logical and arithmetic facts. Our experiments show that SPLIT solves many more of these proof tasks than existing approaches. This suggests that language models can become useful assistants for verifying low-level software with complex memory manipulation.