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, optimization, and verification, yet remains an open challenge for large C++ repositories. Existing LLM-based approaches do not simultaneously scale to such repositories, produce specifications expressive enough to capture systems code features like dynamic memory and heap-allocated data structures, and systematically validate those specifications to rule out incorrect ones. We present Spec-Agent, an agentic system for synthesizing expressive, well-validated specifications across large C++ codebases. Spec-Agent targets a ladder of specification languages: propositional, first-order, propositional separation, and first-order separation logic. For each function, Spec-Agent uses static analysis and runtime heap tracing to select the target specification language, generalizes existing functional tests into fuzz harnesses, and iteratively refines LLM-generated candidates with counterexample-guided feedback. We evaluate Spec-Agent on open-source C++ codebases comprising millions of lines of code. Spec-Agent synthesizes valid specs for 85% of functions, with no false positives observed under fuzzing and expert validation, outperforming Claude Code Opus 4.6 at 10x lower token cost.