Agentic Separation Logic Specification Synthesis

Specification synthesis, the task of automatically inferring formal specifications from program implementations and natural language, is important for refactoring, transpilation, and optimization, yet remains an open challenge for large software repositories. Existing LLM-based approaches fail to simultaneously scale to such repositories, produce specifications expressive enough to capture systems-code features such as dynamic memory and heap-allocated data structures, and systematically validate those specifications to rule out incorrect candidates. We present Spec-Agent, a model-agnostic inference-time method for synthesizing expressive, well-validated specifications across programming languages and large codebases. Spec-Agent targets a ladder of specification languages: propositional logic, first-order logic, propositional separation logic, and first-order separation logic. For each function, Spec-Agent uses static analysis and runtime heap tracing to select the appropriate target specification language, generalizes existing functional tests into fuzz harnesses, and iteratively refines LLM-generated candidates via counterexample-guided feedback. We evaluate the same method on large open-source C++ repositories and a popular open-source Rust codebase. Across the evaluated settings, Spec-Agent synthesizes test-valid specifications for up to $\text{85\%}$ of target functions, with no false positives observed under fuzzing and expert validation in either language, outperforming Claude Code Opus 4.6 at \textbf{10\times} lower token cost.