PaperlayerView exact revision on arXiv

Source-linked AI summary

Local Success Does Not Compose: Benchmarking Large Language Models for Compositional Formal Verification

Xu Xu, Xin Li, Xingwei Qu, Jie Fu, Binhang Yuan

arXiv:2509.23061v1cs.PLcs.AI

TL;DR

Existing benchmarks largely assess isolated-function specifications, leaving compositional reasoning across interacting components underexamined. We introduce DAFNYCOMP, a benchmark of 300 synthesized multi-function Dafny programs. Models show a large syntax-to-verification gap on these tasks, and the benchmark supports analysis of systematic failure modes.

  • Problem

    Existing verification benchmarks primarily evaluate isolated functions, while compositional specification generation across interacting components remains underexamined.

    Source: §1 · p. 2

  • Method

    DAFNYCOMP evaluates specification generation on 300 synthesized multi-function Dafny programs with data dependencies across function boundaries.

    Source: §1 · p. 2

  • Results

    At Pass@8, models average 95.67% syntax correctness but 3.69% verification, and verification gains from Pass@4 to Pass@8 average only 0.8%.

    Source: §4.3 · pp. 7–8

  • Takeaways & Limitations

    DAFNYCOMP provides a diagnostic benchmark for measuring progress toward LLMs that can verify complex multicomponent programs.

    Source: §7 · p. 10

    The benchmark restricts compositions to sequential chains rather than recursive compositions or mutual dependencies, for synthesis tractability.

    Source: §6 · p. 10

Abstract

from arXiv · show

We introduce DafnyCOMP, a benchmark for evaluating large language models (LLMs) on compositional specification generation in Dafny. Unlike prior benchmarks that focus on single-function tasks, DafnyCOMP targets programs composed of multiple interacting functions with data dependencies, requiring reasoning across component boundaries. The benchmark consists of 300 automatically synthesized multi-function programs. We evaluate several state-of-the-art LLM families and find that, while they perform well on single-function verification, their performance drops sharply on compositional tasks. Analysis reveals systematic failures in cross-functional reasoning, including fragile specifications, misalignment between implementations and proofs, and unstable reasoning. DafnyCOMP thus provides a diagnostic tool for measuring progress toward reliable, verifiable, and compositional code generation with LLMs.

1 Introduction

Existing benchmarks largely test specifications for isolated functions, while real programs require correctness across interacting components. DafnyCOMP targets that gap with multi-function Dafny programs and reveals low verification success alongside recurring compositional reasoning failures.

1 Introduction

  • Existing benchmarks focus on isolated functions, leaving compositional specification generation across interacting components untested.Conventional testing also cannot rule out rare corner cases or subtle specification mismatches.Source: §1 · p. 2
  • DAFNYCOMP evaluates 300 Dafny programs formed from 2–5 interacting functions with data dependencies.The benchmark is designed to require reasoning across function boundaries for end-to-end correctness.Source: §1 · p. 2
  • At Pass@8, syntax correctness averages 95.67% while verification averages 3.69%, a 92-percentage-point gap across models.The gap persists across model families, prompt settings, and sampling strategies; even the best model reaches only around 7% verification success after up to eight attempts.Source: §1 · pp. 2–3
  • Fragile specifications can trigger cascading proof failures when one function’s postcondition does not imply a callee’s precondition.Omissions, over- or under-strengthening, and inconsistent framing clauses can invalidate downstream proofs.Source: §1 · p. 3
  • Other recurring failures include implementation–proof misalignment and unstable reasoning that loses invariants or case coverage across steps and function boundaries.DAFNYCOMP is presented as a diagnostic benchmark for measuring progress toward compositional verification of multicomponent programs.Source: §1 · p. 3

2 Related Work

Prior verifiable-code benchmarks either focus on isolated methods or on theorem proving that is disconnected from practical programming. DAFNYCOMP targets compositional specification generation through multi-function programs with data dependencies.

Formal Verification Benchmarks

  • Single-function benchmarks such as DAFNYBENCH and MBPP-DFY assess annotation completion but do not capture interfunction dependencies.They report moderate success rates of 50–60%.Source: §2 · p. 3
  • Interactive theorem-proving benchmarks such as miniCodeProps [22] and FVAPPS target systems like Lean but require extensive manual validation and remain disconnected from practical programming.Source: §2 · p. 3

Dynamic Benchmark Generation

  • Dynamic benchmark generation addresses contamination and overfitting [12] [36], but prior techniques in mathematics and logic [37] [38] neglect formal verification’s demands for valid, precise specifications across execution paths.DAFNYCOMP’s controlled composition generates verifiable multi-function Dafny programs while retaining semantic complexity.Source: §2 · p. 3

Compositional Reasoning in LLMs

  • DAFNYCOMP provides a diagnostic benchmark for formal-verification compositional reasoning by requiring specifications to bridge function boundaries with explicit data dependencies.Formal verification requires invariants to hold across components and global correctness, beyond the pattern-matching emphasis attributed to existing training paradigms.Source: §2 · pp. 3–4

3 Benchmark Construction

DAFNYCOMP constructs mechanically verified, multi-function Dafny programs and evaluates specification reconstruction across function boundaries. Its 300 cases combine chained data dependencies, algorithmic variety, and a substantial verification-annotation burden.

3.1 Program Assembly

  • Program assembly chains 2–5 selected functions so each output feeds the next input, with interface checks and tests filtering compositions before translation.Selection retains functions with cyclomatic complexity above 5 and at least 10 lines; the assembly stage yields 1,200 valid Python programs.Source: §3.1 · pp. 4–5

3.2 Formal Translation

  • Incremental AST-guided translation decomposes Python programs into fragments, verifies each Dafny fragment, then progressively reassembles and refines the program.The pipeline produces 564 verified programs from 1,200 attempts (47%); 300 are retained, balanced across complexity levels.Source: Figure 2 · p. 4, §3.2 · p. 5

3.3 Evaluation Task Format

  • The evaluation removes contract clauses and asks models to reconstruct them, isolating cross-function contract reasoning from implementation concerns.The benchmark spans 15 algorithmic categories; its median program requires 7 loop invariants and 4 assertions, and 23% require intricate termination arguments.Source: §3.3 · p. 6, §3.4 · p. 6

3.4 Benchmark Statistical Summary

  • The benchmark contains 300 mechanically verified Dafny cases covering compositional complexity, algorithmic diversity, and increased specification burden.Programs contain 2–5 functions, averaging 3.2 functions and 8.4 cross-function data dependencies.Source: §3.4 · p. 6

4 Experimental Setup And Results

The evaluation measures syntax correctness and Dafny verification across 13 frontier models on compositional tasks. Models show a large syntax–verification gap, with failures persisting across scaling, sampling, and reasoning-focused approaches.

4.1 Metrics

  • The evaluation uses syntax correctness for parseable specifications and verification rate for the fraction of syntactically valid programs that pass Dafny.Pass@k measures the probability of solving a problem within k attempts, reported for k ∈ {1, 2, 4, 8}.Source: §4.1 · pp. 6–7

4.3 Results and Discussion

  • At Pass@8, syntax correctness is µ = 95.67% (SD = 4.21%) but verification is µ = 3.69% (SD = 2.14%), a 92-percentage-point gap.The gap persists across model scale, training specialization, architectural family, and sampling levels.Source: Table 1 · p. 7, §4.3 · pp. 7–8

4.2 Model Selection

  • The benchmark evaluation covers 13 frontier models spanning five architectural families.The selected models were chosen for demonstrated strength in code generation and general reasoning.Source: §4.2 · p. 7

4.3 Results and Discussion

  • A 3.2× increase in functions accompanies a 14.4× decrease in verification success, from ∼53% on single-function tasks to 3.69% on DAFNYCOMP.The authors suggest specification requirements grow combinatorially with function composition.Source: §4.3 · p. 8
  • From Pass@4 to Pass@8, verification improves only 0.8% on average, while syntax correctness improves 7.3% on average.The verification curve plateaus by Pass@4 across models, unlike syntax correctness.Source: §4.3 · p. 8
  • Reasoning-specialized models show no clear advantage; QWQ-32B achieves 0% verification at Pass@8, and verification rates have a coefficient of variation of 0.58.The authors interpret this clustering as evidence that compositional verification needs different architectural primitives.Source: §4.3 · p. 8

5 Failure Case Analysis and Discussion

Analysis of verification failures identifies three recurring problems: fragile contracts across function boundaries, inconsistency between implementations and specifications, and unstable inductive reasoning.

5 Failure Case Analysis and Discussion

  • The failure analysis examines 900 verification failures across three representative model families, with Table 2 summarizing the failure-mode distribution.Categories were determined through automated error analysis and manual validation on a 10% sample.Source: §5 · p. 8, Table 2 · p. 8

5.1 Specification Fragility: The Domino Effect

  • Locally adequate specifications can fail composition when missing contracts prevent data constraints from propagating between functions.For example, omitting a non-negativity postcondition can make a downstream function’s precondition unprovable despite locally correct components.Source: §5.1 · pp. 8–9

5.2 Implementation–Proof Misalignment: The Independence Assumption

  • In 21.7% of failures, syntactically valid implementations contradict their specifications, including plausible invariants that do not match code behavior.The authors describe code and specifications as being generated independently rather than as coupled constraints.Source: §5.2 · p. 9

5.3 Reasoning Instability: Induction as Achilles’ Heel

  • Models often fail to sustain inductive reasoning through loop iterations, recursive termination arguments, and extensions from base cases.The analysis links this instability to models approximating familiar invariant patterns rather than constructing the required proofs.Source: §5.3 · p. 9

6 Limitations and Future Work

The evaluation is constrained by its compositional patterns, specification types, and available data. The authors identify broader call-graph coverage, other specification properties, and data diversity as future-work directions.

6 Limitations and Future Work

  • The benchmark tests sequential function-call chains, not recursive compositions or mutual dependencies, because of synthesis tractability.Extending coverage to arbitrary call graphs requires addressing verification tractability for cyclic dependencies, which the authors describe as independent of LLM capabilities.Source: §6 · p. 10
  • The benchmark covers functional correctness through preconditions, postconditions, and invariants, but not liveness, resource bounds, or security policies.The excluded concerns require different verification techniques and evaluation metrics.Source: §6 · p. 10
  • Repositories contain few verified multi-function programs with compositional specifications, and synthetic-data approaches still face a semantic-diversity challenge.The authors suggest synthetic data generation or bootstrapped program synthesis as possible ways to address data scarcity.Source: §6 · p. 10

7 Conclusion

DAFNYCOMP evaluates compositional specification generation on synthesized multi-function Dafny programs. The reported results show a sharp verification gap between single-function and compositional tasks, while the paper also discloses a language-model use limited to editorial refinement.

7 Conclusion

  • Greater than 99% syntax correctness and more than 58% single-function verification contrast with 3.69% verification on compositional tasks, a 92% degradation.The performance cliff persists across model families despite increased sampling (Pass@8).Source: §7 · p. 10
  • DAFNYCOMP comprises 300 synthesized multi-function Dafny programs used to assess 13 state-of-the-art LLMs on correctness across function boundaries.The conclusion identifies the benchmark as a diagnostic tool and a target for future research.Source: §7 · p. 10

A The Use of LLMs in Writing

  • GPT-5 was used only for language refinement and editorial improvements; the research design, experiments, analysis, and core intellectual contributions remained original.Source: A The Use of LLMs in Writing · p. 13

B Broader Impact and Societal Implications

The paper discusses possible benefits and risks of automated verification, including reliability applications, deployment cautions, and access and computational costs. It also describes Dafny’s integrated verification approach and why reasoning across composed components matters.

B Broader Impact and Societal Implications

  • Automated verification could enhance reliability in safety-critical systems and make formal methods more accessible to resource-constrained teams.Source: B Broader Impact and Societal… · p. 13
  • The authors warn that the documented 92% verification failure rate counsels against premature deployment in safety-critical contexts.They also note that fragile specifications could create false confidence in system safety.Source: B Broader Impact and Societal… · p. 13
  • The benchmark is open-source, but evaluating frontier models requires costly API access, and evaluation across 13 LLMs carries computational costs.The paper also emphasizes continued human expertise in safety-critical software development.Source: B Broader Impact and Societal… · p. 13

C Introduction to Dafny

  • Dafny integrates an automated verifier into development, enabling developers to construct code mathematically proven to satisfy specifications.Its specifications include preconditions, postconditions, and logical properties; an example annotates an array method with such conditions.Source: C Introduction to Dafny · p. 13
  • Reasoning about composed verified components determines whether verification can scale beyond small, isolated programs to real-world systems.Source: C Introduction to Dafny · p. 13

D Automated Theorem Proving

The section contrasts automated verification with interactive theorem proving and outlines Dafny’s proof pipeline. It also presents prompts for generating and debugging Dafny specifications from Python code.

D Automated Theorem Proving

  • Dafny and Verus use SMT solvers to discharge proof obligations with lightweight annotations, while interactive theorem provers expose proof steps for iterative refinement and diagnosis.The paper positions Dafny as combining code, specifications, and automated verification in a setting close to mainstream programming practice.Source: D Automated Theorem Proving · p. 14
  • Dafny translates code and specifications into Boogie verification obligations, which an SMT solver processes to check validity.A successful proof confirms correctness according to the specifications; failed proofs provide feedback on inconsistencies.Source: D Automated Theorem Proving · p. 14
  • Table 3 is presented as comparing Dafny and Python, with the surrounding text framing the contrast around their design philosophies and primary objectives.Source: D Automated Theorem Proving · p. 14, Table 3 · p. 14

E Prompt for Synthesis

  • The initial synthesis prompt asks for Python-to-Dafny translation with method signatures, preconditions, postconditions, verification details, and a self-contained verified snippet.It also requests explanations of invariant choices and how they support loop correctness.Source: E Prompt for Synthesis · p. 15
  • The dynamic debugging prompt asks the model to diagnose verification errors and fix the main-function specification so it parses successfully.The prompt supplies the Dafny code and verifier error message as context.Source: E Prompt for Synthesis · p. 16

F Data Contamination Analysis

The analysis compares DafnyCOMP source data with MBPP and finds no significant overlap across four configurations, supporting the benchmark’s integrity.

F Data Contamination Analysis

  • The analysis compared the benchmark source data against MBPP and found no significant overlap.MBPP is identified as a widely used dataset for assessing contamination in Python source data.Source: F Data Contamination Analysis · p. 16
  • The code-only analysis used Exact Match for verbatim copies and n-gram Jaccard Similarity for structurally similar code.The results cover four distinct configurations summarized in Table 4.Source: F Data Contamination Analysis · p. 16
  • All configurations produced zero exact matches, and n-gram Jaccard similarity peaked at 0.0078 under the most aggressive settings.The authors describe this as strong evidence that DAFNYCOMP is free from training data contamination.Source: F Data Contamination Analysis · p. 16

G Prompt for Evaluation

The evaluation appendix specifies a code-only Dafny prompting protocol and reports contamination results alongside examples of failures in generated specifications, proofs, and code.

G Prompt for Evaluation

  • Table 4 compares DAFNYCOMP with MBPP under four configurations and reports zero exact matches and negligible n-gram similarity.The configurations range from conservative, default, and aggressive preprocessing to a holistic structure-level check.Source: Table 4 · p. 17
  • The prompt asks models to fill missing annotations while preserving given signatures and contracts, and their outputs are used directly for Dafny verification.It requests code only, including loop invariants and assertions where needed.Source: G Prompt for Evaluation · p. 17

H.1 Challenge 1: Formal Specification Synthesis

  • Specification-synthesis examples include an unproved postcondition on digitSum and an unproved precondition at a call.The appendix frames these as failures involving preconditions and postconditions.Source: §H.1 · p. 18, §H.1.1 · p. 18, §H.1.2 · p. 18

H.2 Challenge 2: Ensuring Code Correctness

  • Code-correctness examples show a loop invariant failing on entry and an assertion that might not hold.These are presented as implementation issues where code logic does not satisfy the specifications.Source: §H.2 · p. 18, §H.2.1 · p. 19, §H.2.2 · p. 19

H.3 Challenge 3: Proof Generation and Formal Reasoning

  • Proof-generation examples include an invariant not maintained in stringToInt and an unproved recursive termination condition for gcd_func.The examples concern loop invariants and formal proofs.Source: §H.3 · p. 20, §H.3.1 · p. 20, §H.3.2 · p. 20

H.4 Challenge 4: Spec-Code-Proof Alignment

  • Spec–code–proof alignment breaks when methods are used in expression contexts, which Dafny rejects for stringToInt and isBeautiful.The appendix identifies method-versus-function usage as the source of these examples’ misalignment.Source: §H.4 · p. 21, §H.4.1 · p. 21, §H.4.2 · p. 22

H.5 Challenge 5: Complexity and Scalability Issues

  • The scalability category includes a large-array example whose loop invariant cannot be proved on entry.The appendix introduces this category as involving complex programs or large data structures.Source: §H.5 · p. 23, §H.5.1 · p. 23

H.6 Challenge 7: Avoiding Trivial Solutions; H.7 Challenge 8: Limited Training in Formal Domains

  • Trivial-solution cases were sparsely represented and include weak or incomplete specifications, while syntax examples show Dafny type and parse errors.The appendix also describes limited training in formal domains as a challenge category.Source: §H.6 · p. 24, §H.7 · p. 24

H.7.1 Example 8.1: Parse Error (org_input_id: 0, self_id: 0)

The two examples show generated Dafny code failing to parse: one uses an unsupported string type, and both report two parse errors.

H.7.1 Example 8.1: Parse Error (org_input_id: 0, self_id: 0); H.7.2 Example 8.2: Syntax Error (org_input_id: 0, self_id: 2)

H.7.1 Example 8.1: Parse Error (org_input_id: 0, self_id: 0)

  • Example 8.1 declares stringToInt with a string input, which Dafny rejects, and reports two parse errors.The error message recommends using seq<char> instead.Source: §H.7.1 · p. 24, §H.7.2 · p. 25

H.7.2 Example 8.2: Syntax Error (org_input_id: 0, self_id: 2)

  • Example 8.2 reports two parse errors for a stringToInt method whose input is seq<char>.Its code also includes digit and character conversion helpers and a loop that accumulates digits into the result.Source: §H.7.2 · p. 25

Related papers

Loading 2509.23061v1…