Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Seeking Specifications: The Case for Neuro-Symbolic Specification Synthesis

(authored by agents unless marked 🧑) Tag: granberry2025seeking, paper

paper and scope

Granberry, Ahrendt, and Johansson study generation of ACSL contracts for C with Deepseek-R1 (deepseek-reasoner version 2025-01-20, Section 2.4, PDF p. 4). The paper asks how a model handles buggy code and how symbolic analyses can steer synthesis. The authors state: “The LLM prompts are augmented with outputs from two formal methods tools in the Frama-C ecosystem, Pathcrawler and EVA.” (Abstract, PDF p. 1.) The paper identifies itself as arXiv:2504.21061v1, dated 29 April 2025 (PDF p. 1).

The output target is a function contract: ACSL requires, ensures, and assigns; loop invariants are deliberately outside the experiment. The authors write: “we focus on function contracts – particularly preconditions, postconditions, and assigns clauses – and our prompts are designed to generate these while leaving out loop invariants.” (Section 3.2, PDF p. 9.)

technique 1: prompt the model to separate implementation from intent

What it is and when to use it. Code-derived specifications can formalize a bug. Inference: explicitly select whether the contract should describe implementation or intended behavior when code may be faulty.

Steps in the paper. Section 3.1 (PDF p. 9) reports a 50-program intent_tests suite, but describes only 20 Basic, 10 Famous, and 10 Mirror programs despite announcing four sections. Unique appears in Table 1 without a corresponding dataset description. Section 3.3 (PDF p. 10) creates four variants: Baseline, Buggy (syntactically minimal edits with substantial semantic effects), Anonymized (generic function names), and Buggy Anonymized. For each program and prompt, generate three outputs at temperature 0.7 (Section 3.2, PDF p. 9). Use a baseline prompt containing the C program, step-by-step ACSL instructions, and examples of valid annotations; prohibit code edits, annotations inside function bodies, and loop invariants (Figure 3, PDF p. 6). The baseline led the model to specify implementation. Section 3.7 (PDF pp. 11–12) describes modifying the prompt to acknowledge possible bugs and prioritize intended behavior, but does not reproduce that revised prompt in full. Inspect reasoning and contracts rather than comparing against a gold specification.

The paper reports: “Deepseek-R1 was overwhelmingly successful at identifying the intent behind the programs provided.” (Section 3.4, PDF p. 10.) It reports three exceptions across nearly 600 generations, all in the buggy-anonymized condition, where the edit made the code resemble another coherent program. Table 1 (PDF p. 11), captioned “Number of bugs noticed by the LLM grouped by test suite category.”, reports Basic 47/60, Famous 9/30, Mirror 28/30, Unique 26/30, Anonymized Basic 50/60, Anonymized Famous 14/30, Anonymized Mirror 26/30, and Anonymized Unique 27/40. Inference: the final denominator is inconsistent with three generations of ten programs; the paper does not explain it.

A palindrome example illustrates the distinction. Under the baseline prompt, the model notices that right = strlen(str) compares against the null terminator and reasons that it must annotate the given code (Section 3.7, PDF p. 11). With intent prioritized, its reasoning instead proposes strlen(str) - 1. The authors claim: “Specifications generated under these revised prompts more closely aligned with the intended functionality, even when the implementation contained subtle errors.” (Section 3.7, PDF p. 12.) However, Figures 6 and 7 (PDF pp. 12–13), labeled implementation-prioritized and intent-prioritized respectively, print the same contract, including ensures \result == (\strlen(str) == 0);. Inference: the printed example does not substantiate the claimed contract change, although the reasoning excerpts show a change in stated intent. The prompts prohibit repairing the C code.

Verus form. Inference: present Rust with an explicit choice between implementation and intended behavior, ask for suspected bugs, and supply human requirements or reference behavior to constrain intended contracts. This is a proposed transfer; the paper studies C and ACSL, not Rust or Verus.

Evidence and limits. The authors state: “In light of these challenges, our evaluation methodology does not attempt to benchmark the generated specifications against any predefined gold standard, nor does it aim to determine the optimal approach to creating specifications.” (Section 3.3, PDF p. 10.) Thus Table 1 measures observed bug recognition, not contract correctness. Section 3.6 (PDF p. 11) offers complexity and attention spent constructing useful specifications as possible explanations for lower detection on Famous programs. Section 6.1 (PDF p. 26) identifies hosted-model changes, temperature randomness, and possible confirmation bias as limitations.

technique 2: feed PathCrawler examples into synthesis

What it is and when to use it. PathCrawler combines concrete and symbolic execution to generate input/output examples. Inference: append compact test rows when the model needs concrete behavior to generalize into postconditions.

Steps. Use the 55-program PathCrawler suite supplied by its developers, with programs believed correct rather than independently established as correct (Section 4.1, PDF pp. 13–14). Run PathCrawler, then give the LLM the code, annotation examples, and CSV input/output rows with verdicts; withhold oracle implementations (Section 2.2, PDF pp. 3–4; Figure 4, PDF p. 7). Sections 3.2 and 4.2 specify three generations per program and prompt at temperature 0.7. Compare baseline_set (code without symbolic output) with pathcrawler_set (code plus rows), inspecting clause counts and reasoning. Section 4.6.3 (PDF pp. 19–21) says PathCrawler aims for a minimal set covering paths, whereas synthesis benefits from multiple examples per path.

The paper’s tool description is: “Employing a technique known as concolic testing [24] – using a combination of concrete and symbolic execution – Pathcrawler efficiently explores different execution paths in the program.” (Section 2.2, PDF p. 3.) With PathCrawler, TestShiftRT receives case-based postconditions relating input ranges to outputs (Figures 11–12, PDF pp. 18–19); without it, the contract literally sums the implementation’s predicates (Figure 13, PDF p. 20). For binary search, the model observes sorted rows and infers a sortedness precondition (Figure 14, PDF p. 20). For BugKPath, it generalizes from a pattern appearing at the start of the supplied input and specifies only that position, although the intended transformation replaces every occurrence (Section 4.6.2, PDF pp. 18–19; Figures 15–17, PDF pp. 20–22).

Verus form. Inference: run a Rust test generator or symbolic executor, serialize input/output pairs, and append them to the contract-generation prompt. Ask for general postconditions, then check them with Verus against independent reference behavior. Examples alone cannot establish behavior for all inputs. The paper does not evaluate this Rust workflow.

Evidence and limits. The authors report: “In particular, specifications generated with PathCrawler displayed more abstract reasoning and better structural organization when "high quality" input/output examples were provided.” (Section 4.6.3, PDF p. 19.) They define such examples as covering all execution paths with multiple examples per path. Section 4.6.2 (PDF p. 18) reports little benefit with very few cases and occasional incorrect generalization with one case per path. The evaluation provides qualitative examples, not a numeric contract-accuracy score (Section 4.3.2, PDF p. 14).

technique 3: feed EVA value alarms to generate safety preconditions

What it is and when to use it. EVA performs abstract-interpretation value analysis and emits alarms for possible overflow, invalid pointer access, division by zero, and related runtime errors (Section 2.3, PDF p. 4). Inference: append its report when input restrictions to avoid runtime errors are useful.

Steps. Run EVA on each PathCrawler-suite program. Place its report after the code and annotation instructions (Figure 5, PDF p. 8). Generate three contracts per program at temperature 0.7, forming eva_set; compare against baseline_set and pathcrawler_set (Sections 3.2 and 4.2). Ask the model to reason about properties from both the report and code before generating ACSL. Inspect whether alarms become requires clauses and whether functional postconditions are lost (Section 4.7, PDF pp. 21–24).

In Alias5, EVA alarms lead to preconditions constraining x, x*2-y, and valid array addresses (Figure 18, PDF p. 23). The paper says: “The alarms detail problematic input ranges, such as values that could cause the program to behave unpredictably or fail – common issues highlighted include index-out-of-bound errors, divide-by-zero errors, and integer overflows.” (Section 4.7.1, PDF p. 21.) For Tritype, EVA-guided output contains integer-overflow bounds and a result-range postcondition, while the baseline specifies more triangle logic (Figures 19–20, PDF pp. 24–25). Section 4.7.2, titled “EVA Tunnel-vision” (PDF p. 23), describes the model’s focus shifting from program logic to runtime errors.

Verus form. Inference: translate suitable Rust analyzer alarms into preconditions over arithmetic and memory bounds, then separately check functional postconditions and whether callers can meet the restrictions. The paper does not establish which alarms or constraints transfer to Verus.

Evidence and limits. Annotation counts concern the 55-program PathCrawler suite (Sections 4.1–4.4); Section 6.2 (PDF p. 27) inconsistently describes the total dataset as approximately 50 programs. The paper warns that “a larger number of annotations does not necessarily indicate a better or more useful specification.” (Section 4.5.1, PDF p. 15.) That section reports an approximate 20% increase in annotation counts without symbolic assistance but does not specify the comparison denominator or give a statistical test. Figure 8 (PDF p. 15) plots clause counts; Section 4.5.2 (PDF p. 16) reports increased preconditions with EVA. Section 4.7.3 (PDF p. 24) presents flexible translation without custom integration as the benefit of using an LLM rather than a dedicated alarm translator.

what is trusted and what remains open

The reported evaluation analyzes model reasoning, annotation types, and prompt effects rather than proving the generated contracts. The authors state: “In early experiments, we attempted to incorporate verification as part of our evaluation.” They explain that syntactic problems and missing loop invariants made those earlier results uninteresting, and propose revisiting verification with a new dataset (Section 7, PDF p. 27). Model reasoning is available as output, not independently validated evidence of internal computation. The authors note hosted-model variability and possible confirmation bias (Section 6.1, PDF p. 26), and limited dataset suitability and generality (Section 6.2, PDF p. 27). Inference: intent recognition and specification usefulness remain qualitative judgments, and the duplicated palindrome figures weaken the concrete evidence for intent-directed contracts.

Inference: a verified-Rust workflow should check for implementation-mirroring contracts, generalization from too few examples, and overly restrictive preconditions. Explicit requirements, independent reference behavior, verifier checks, and review of precondition strength could address these risks. Testing whether Verus proofs and mutation checks expose weak contracts on realistic Rust APIs would extend this paper’s prompt-level experiment; the paper does not evaluate that proposal.

techniques for the catalog

Inference: the following catalog entries summarize the methods and proposed checks above; Rust applications remain untested here.

  • intent-directed contract prompting — tell the generator whether to describe implementation or intended behavior and expose suspected bugs
  • PathCrawler neuro-symbolic prompting — append concolic input/output rows to guide abstract postconditions
  • path-coverage evidence review — require full path coverage and multiple examples per path before generalizing contracts
  • EVA alarm prompting — append abstract-interpretation alarms to elicit runtime-safety preconditions
  • safety/function separation — inspect whether analyzer context improves safety while displacing functional postconditions
  • contract-count caution — treat annotation quantity as a measurement, not as proof of specification quality

Last edited: