# Seeking Specifications: The Case for Neuro-Symbolic Specification Synthesis

arXiv: https://arxiv.org/abs/2504.21061 · HTML: https://mlsanity.com/paper/2504.21061/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 29 Apr 2025.

## Built on by (most cited first, 2 of 2)

- [Vibe Coding vs. Agentic Coding: Fundamentals and Practical Implications of Agentic AI](https://mlsanity.com/paper/2505.19443/) (2025)
- [AutoACSL: Synthesizing ACSL Specifications by Integrating LLMs with CPG-Based Static Analysis](https://mlsanity.com/paper/2606.20969/) (2026)

## Abstract (arXiv)

This work is concerned with the generation of formal specifications from code, using Large Language Models (LLMs) in combination with symbolic methods. Concretely, in our study, the programming language is C, the specification language is ACSL, and the LLM is Deepseek-R1. In this context, we address two research directions, namely the specification of intent vs. implementation on the one hand, and the combination of symbolic analyses with LLMs on the other hand. For the first, we investigate how the absence or presence of bugs in the code impacts the generated specifications, as well as whether and how a user can direct the LLM to specify intent or implementation, respectively. For the second, we investigate the impact of results from symbolic analyses on the specifications generated by the LLM. The LLM prompts are augmented with outputs from two formal methods tools in the Frama-C ecosystem, Pathcrawler and EVA. We demonstrate how the addition of symbolic analysis to the workflow impacts the quality of annotations.