Breaking the Composition Cliff: Mutation-Guided Specification Synthesis for Multi-Function Programs

Large language models (LLMs) can generate code, but synthesizing formal specifications for this code remains challenging. While previous approaches report high verification rates on individual functions, real-world programs are composed of modular interprocedural call graphs. We evaluate six frontier language models on synthesizing formal Dafny specifications for 300 multi-function programs with call-graphs of sizes 2–5 (DafnyComp-300), revealing two key shortcomings. First, we find that models struggle with compositional specifications: while models reach 91.7%–100% specification completeness on individual functions with repair, zero-shot specification success collapses from up to 95.0% on single functions down to 14.0%–41.3% on multi-function call graphs. Second, the traditional repair loop, which relies on compiler error messages, leads models to learn vacuous specifications, e.g., trivial inequalities such as ensures res >= 0. While these specifications appear logically sound, they are overly weak and cannot reject incorrect implementations. To address this, we present Mutation-CEGIS, an approach that uses AST code mutants to test specifications for vacuity. When a candidate specification mistakenly admits a buggy mutant, we extract the code change as a concrete counterexample for the model to refine its specification. On single-function benchmarks (CloverBench-60), Mutation-CEGIS boosts specification completeness to 91.7%–100.0% while reducing repair turns by up to 36.8% and saving up to 24.9% of total tokens. On compositional call graphs (DafnyComp-300), Mutation-CEGIS systematically detects vacuous bounding contracts across all model families and, when synthesis succeeds, drives models toward tighter first-order relational specifications (∀, ∃). Finally, we find that for deeper call-graphs, exact specification synthesis results in SMT-solver timeouts, demonstrating that future verification agents will benefit from synthesizing auxiliary lemmas in addition to specifications.