Agentic Separation Logic Specification Synthesis

2026-05-26 · Tarun Suresh, David Korczynski, Julien Vanegue arxiv

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 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, an agentic system for synthesizing expressive, well-validated specifications across large C++ 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 Spec-Agent on open source C++ codebases comprising millions of lines of code. Spec-Agent synthesizes valid specifications for 85% of target functions, with no false positives observed under fuzzing and expert validation, outperforming Claude Code Opus 4.6 at 10x lower token cost.

📄 PDF Abstract BibTeX arXiv:2605.27531

Code (0)

등록된 구현이 없습니다.

Guiding LLM Temporal Logic Generation with Explicit Separation of Data and Control

2024-06-11 · William Murphy, Nikolaus Holzer, Nathan Koenig, Leyi Cui 외

Temporal logics are powerful tools that are widely used for the synthesis and verification of reactive systems. The recent progress on Large Language Models (LLMs) has the potential to make the process of writing such sp…

Program Synthesis

Modularized Control Synthesis for Complex Signal Temporal Logic Specifications

2023-03-30 · Zengjie Zhang, Sofie Haesaert

The control synthesis of a dynamic system subject to a signal temporal logic (STL) specification is commonly formulated as a mixed-integer linear/convex programming (MILP/MICP) problem. Solving such a problem is computat…

Containment Verification: AI Safety Guarantees Independent of Alignment

2026-05-09 · Royce Moon, Lav R. Varshney arxiv

Agentic frameworks are the software layer through which AI agents act in the world. Existing safety methods intervene on the model and therefore remain conditional on unverifiable properties of learned behavior. We intro…

Scaling the Scaling Logic: Agentic Meta-Synthesis of Logic Reasoning

2026-01-23 · Bowen Liu, Zhi Wu, Runquan Xie, Zhanhui Kang 외 arxiv

Reinforcement Learning from Verifiable Rewards (RLVR) is bottlenecked by data: existing synthesis pipelines rely on expert-written code or fixed templates, confining growth to instance-level perturbations. We shift the e…

Reinforcement Learning

Agentic Framework for Epidemiological Modeling

2026-01-30 · Rituparna Datta, Zihan Guan, Baltazar Espinoza, Yiqi Su 외 arxiv

Epidemic modeling is essential for public health planning, yet traditional approaches rely on fixed model classes that require manual redesign as pathogens, policies, and scenario assumptions evolve. We introduce EPIAGEN…