DafnyCert: Certifying Specification Strength in Dafny

DafnyCert: Certifying Specification Strength in Dafny

arXiv:2611.15548v1 [cs.SE] 11 Nov 2026

ÁLVARO SILVA, Faculdade de Engenharia, Universidade do Porto, Portugal ISABEL AMARAL, Faculdade de Engenharia, Universidade do Porto, Portugal RUBEN MARTINS, Carnegie Mellon University, USA ALEXANDRA MENDES, Faculdade de Engenharia, Universidade do Porto, Portugal Formally verifying a method with Dafny guarantees correctness relative to its specification. However, a specification may be too permissive, allowing multiple outputs for the same input, even when the implementation produces only one. In this scenario, a different implementation could produce a different result while still satisfying the same specification. Therefore, successful verification does not necessarily establish that the method behaves as intended. In this paper, we propose checkable certificates that provide independently verifiable evidence of whether a specification is weak or strong. A certificate of weakness contains an alternative implementation that verifies against the original specification, together with a witness input on which the original and alternative implementations produce different results. A certificate of strength is produced by constructing a harness around the original method such that successfully verifying the harness guarantees that the specification allows at most one possible output for any given input. We present DafnyCert, a tool that automatically produces these certificates. Strength is established by constructing and verifying the harness. Weakness is demonstrated by using the MutDafny mutation tool to find mutants that verify against the original specification, and by using the Hypothesis property-based testing framework to generate inputs that produce different outputs for the original program and the mutant. The resulting mutant and witness form a recheckable certificate of weakness. We reduce the cost of mutation-based search by selecting a smaller set of operators that generates only 22.7% of the mutants on the selection set, covering 91.6% of the 2,841 weak specifications of VeriEquivBench in an independent transfer set. On a dataset of 3,910 verified Dafny methods from Dafny-Synthesis and VeriEquivBench, DafnyCert automatically certifies 3,570 methods (91.3%). We also provide certificates for the remaining 340 methods, all accepted by the same validator. To our knowledge, this is the first dataset in which every specification is backed by a checkable certificate of strength or weakness. These labels disagree with the benchmarks’ original labels for 16.3% of the methods. Among single-method VeriEquivBench files, 70.2% of the specifications labeled strong are certified weak, and in Dafny-Synthesis, whose labels were manually assigned, 19 of the 20 disagreements also correspond to specifications labeled strong but certified weak. These findings highlight the importance of supporting specification strength labels, whether assigned by humans or automated methods, with independently checkable evidence. CCS Concepts: • Theory of computation → Logic and verification; Program specifications. Additional Key Words and Phrases: Specification strength, Dafny, formal verification, checkable certificates, mutation testing

1

Introduction

Formal verification has been used to establish the functional correctness of real systems, such as an operating system kernel [13], a C compiler [18], distributed systems [11], and a cryptographic library [27]. Verification-aware languages such as Dafny [17], Why3 [7], and Verus [15] bring these techniques to everyday code, where the developer provides preconditions (requires) and postconditions (ensures) for a method, and an SMT solver [4] checks that the implementation satisfies the specification. Authors’ Contact Information: Álvaro Silva, Faculdade de Engenharia, Universidade do Porto, Porto, Portugal, amfpsilva@hotmail.com; Isabel Amaral, Faculdade de Engenharia, Universidade do Porto, Porto, Portugal, isabel.andre.amaral@gmail.com; Ruben Martins, Carnegie Mellon University, Computer Science Department, Pittsburgh, USA, rubenm@andrew.cmu.edu; Alexandra Mendes, Faculdade de Engenharia, Universidade do Porto, Porto, Portugal, alexandra@archimendes.com.

2

Álvaro Silva, Isabel Amaral, Ruben Martins, and Alexandra Mendes

Successful verification establishes that an implementation satisfies its given specification, but does not ensure that the specification accurately captures the intended behavior. When a specification is too permissive, it can be satisfied by multiple implementations with different behaviors. Thus, the verifier may accept implementations whose behavior differs from the programmer’s intent. This problem arises in real verified systems. Fonseca et al. [8] studied three formally verified distributed systems and identified faults in their specifications. In IronFleet [11], a distributed system written in Dafny, the specification of the replicated state machine did not require exactly-once semantics, even though the implementation provided them. Consequently, the authors managed to disable request deduplication with a small patch that inserted a bug, but still verified against the original specification. The authors conclude that formal verification requires techniques to test specifications. Specification bugs have since been reported in other verified systems. CompCert’s PowerPC semantics did not constrain the width of an immediate field [25], and IronSpec [10] uncovered ten specification bugs in six verified Dafny systems, each of which admitted an incorrect implementation that still verified. This problem has become increasingly relevant as LLMs are used to generate both code and specifications in verification-aware languages. Existing benchmarks for this task, such as DafnySynthesis [21] and VeriEquivBench [26], classify specifications as strong or weak, providing labels for evaluating specification generation and assessment tools. However, these labels are assigned by human annotators or LLMs and may contain errors. Prior work on VeriEquivBench [26] introduced a strong specification checker, which we refer to as VEB-Check, that can automatically prove that a specification is strong, but cannot establish that a specification is weak. Other approaches, including mutation scores [2, 16], proof coverage [28], and LLM judges [24], provide only heuristic assessments rather than checkable guarantees. We argue that specification strength should be determined by independently verifiable evidence. A specification is weak if two implementations that verify against it return different outputs for the same valid input. In this work, to show weakness, we provide a second implementation and an input on which the output differs from that of the original implementation. Running both implementations on that input provides concrete evidence that the specification is weak. A specification is strong when no such pair exists. To show strength, we provide a harness that is verifiable by Dafny only if the specification allows at most one output for each input. We call each of these self-contained artifacts a certificate. Both certificate types, weak and strong, can be checked with dafny verify and dafny run, without trusting any of the tools used to generate them. We built DafnyCert to automatically generate these certificates. It first attempts to prove that a specification is strong. If it fails, it searches for evidence of weakness by mutating the implementation, retaining the verified mutants, and running them on inputs generated from the precondition. The main contributions of this paper are: ▶ A fully certified benchmark dataset for evaluating specification strength in Dafny. We

provide certificates of strength or weakness for 3,910 methods from the Dafny-Synthesis [21] and VeriEquivBench [26] datasets. Each carries either an executable counterexample showing that the specification is weak (certified weak), or a verifiable proof that it is strong (certified strong). The certified labels differ from those in the existing benchmarks for 9.2% (20/218) of Dafny-Synthesis and 16.7% (618/3,692) of VeriEquivBench. ▶ An automated method to certify specifications as weak. We search for an alternative implementation by mutating the method, verifying each mutant against the unchanged contract, and running the mutants that verify on inputs generated from the method’s preconditions. This is enough to automatically certify 91.9% (3,055/3,323) of the weak specifications. ▶ A certificate template and validator. The validator checks certificate integrity and

DafnyCert

3 1 2 Certify Strong (○– ○) on every method 1 generate ○ harness 𝐻 (𝑆)

method 𝑀 + spec 𝑆

2 verify 𝐻 (𝑆) ○ with Dafny

yes

C no

9 Validator ○ re-checks with Dafny, rejects tampering

certified weak / strong

uncertified heuristic label only

strength not proved

still uncertified

3 8 Certify Weak (○– ○) 3 Hypothesis: ○ sample admissible inputs, record 𝑀’s outputs

4 MutDafny: ○ mutate 𝑀, verify each mutant against 𝑆

5 alive ○ mutants

6 run alive ○ mutants on the sample, compare outputs

7 build a ○ certificate per divergence, check it

yes

C

no

8 mutation ○ score heuristic classification weak / strong

4 and ○ 6 on yes, stop ○ 4 and ○ 6 run concurrently: ○ 6 reads ○ 5 while ○ 4 fills it ○

Fig. 1. The DafnyCert pipeline.

re-checks the evidence using Dafny. Trusting a certificate generated from a template only requires trusting the validator and Dafny. ▶ DafnyCert, an end-to-end framework for sound specification strength certification. By extending VEB-Check and integrating our approach for certifying specification weakness, DafnyCert generates certificates for 91.3% (3,570/3,910) of all methods across Dafny-Synthesis and VeriEquivBench. The remaining certificates that complete the dataset, pass the same validator, making the final benchmark fully labeled by re-checkable evidence. 2

DafnyCert

Figure 1 shows the DafnyCert pipeline, which comprises three components. The Certify Strong 1 ○), 2 the Certify Weak approach (○– 3 ○), 8 and the Certificate Validator (○). 9 The pipeline approach (○– takes as input a method 𝑀 and its specification 𝑆, and outputs either a certificate of strength, such as the one in Listing 1, or a certificate of weakness, such as the one in Listing 2. In each, the shaded block is the target method, copied and unchanged from the benchmark, and every other block is the certificate, tagged with the Dafny command that checks it. Both approaches are fully automatic. We first run Certify Strong on every method and Certify Weak on every method it does not certify. Every certificate, regardless of its source, must pass the validator, which detects tampering and unsound constructs. In Figure 1, each diamond marked C is a certificate candidate check. A candidate that passes it (yes) goes to the validator, and one that fails it (no) is discarded, moving the pipeline on to its next stage. Only after passing validation is the specification registered as weak or strong. If no certificate is found, the method is given a heuristic 8 label using the mutation score (○). 2.1

Definition of Weak and Strong Specifications

Informally, a specification is weak if it accepts two distinct programs that disagree on some input, and strong if it determines a unique behavior for every admissible input. We assume throughout the paper that methods, denoted by 𝑀, are deterministic. This assumption is necessary for our notion of strength. Without it, a single implementation could produce different outputs on the same input, so differing outputs would not establish the existence of two distinct implementations. Consequently, randomized algorithms that produce nondeterministic outputs are outside the scope of this formalization.

4

Álvaro Silva, Isabel Amaral, Ruben Martins, and Alexandra Mendes

Listing 1. A proved_strong certificate for DafnySynthesis’s addPairwise (task_id_470, RQ2-GPT4), which the benchmark correctly labels as strong.

Listing 2. A witness_weak certificate for VeriEquivBench’s AddMinimumRungs (task_id_1936, Medium), which the benchmark labels as strong.

method addPairwise(n: seq<int>) returns (res:seq<int>) requires n != [] ensures |n| == 0 ==> |res| == 0 ensures |n| > 0 ==> |res| == |n| - 1 ensures forall i :: 0 <= i < |res| ==> res[i] == n[i] + n[i + 1] { var result: seq<int> := []; var i: int := 0; while i < |n| - 1 // 3 invariants { result := result + [n[i] + n[i + 1]]; i := i + 1; } res := result; }

method AddMinimumRungs(rungs: array<int>, dist: int) returns (result: int) requires rungs.Length >= 1 requires dist >= 1 requires forall i :: 0 <= i < rungs.Length ==> rungs[i] >= 1 requires forall i, j :: 0 <= i < j < rungs.Length ==> rungs[i] < rungs[j] ensures result >= 0 // weak postcondition { result := 0; var currentHeight := 0; for i := 0 to rungs.Length /* 5 invariants */ { var targetHeight := rungs[i]; var gap := targetHeight - currentHeight; if gap > dist { var rungsNeeded := (gap - 1) / dist; result := result + rungsNeeded; } currentHeight := targetHeight; } }

▲ target method 𝑀 and specification 𝑆, unchanged from the benchmark ▼ certificate: the harness 𝐻 (𝑆 ). dafny verify checks 𝑀 |= 𝑆 and that 𝐻 (𝑆 ) verifies

///// FILLED IN HELPERS (empty) /////

// top level

// Predicate generated from addPairwise's `requires', verbatim. ghost predicate addPairwise_Pre(n: seq<int>) { n != [] } method addPairwise_check(n_original: seq<int>, n_mutant: seq<int>) returns (res_original: seq<int>, res_mutant: seq<int>)

{

}

requires addPairwise_Pre(n_original) requires addPairwise_Pre(n_mutant) requires n_original == n_mutant // inputs agree ensures res_original == res_mutant // so must outputs ///// FILLED IN PROOF BEFORE ORIGINAL CALL (empty) ///// res_original := addPairwise(n_original); ///// FILLED IN PROOF BEFORE MUTANT CALL (empty) ///// res_mutant := addPairwise(n_mutant); ///// FILLED IN PROOF BEGIN (hints only; no assume) ///// // FROM mode not-automatic assert |res_original| == |res_mutant|; forall i | 0 <= i < |res_original| ensures res_original[i] == res_mutant[i] { assert res_original[i] == n_original[i] + n_original[i + 1]; assert res_mutant[i] == n_mutant[i] + n_mutant[i + 1]; } ///// FILLED IN PROOF END /////

▲ target method 𝑀 and specification 𝑆, unchanged from the benchmark ▼ certificate: the mutant 𝑀 ′ . dafny verify checks 𝑀 |= 𝑆 and 𝑀 ′ |= 𝑆

///// FILLED IN HELPERS (empty) ///// // top level method AddMinimumRungs_mutant(rungs: array<int>, dist: int) returns (result: int) ... // regenerated, byte-compared { ///// FILLED IN COUNTEREXAMPLE BEGIN (no assume) ///// // FROM mode dafnycert result := 0; ///// FILLED IN COUNTEREXAMPLE END ///// } ▼ certificate: the witness 𝑥 0 . dafny run checks 𝑥 0 ∈ 𝑋𝑃 and 𝑀 (𝑥 0 ) ≠ 𝑀 ′ (𝑥 0 )

method {:verify false} Main() { ///// FILLED IN WITNESS BEGIN (inputs only) ///// // FROM mode dafnycert var rungs_original: array<int> := new int[] [463]; var dist_original: int := 1; var rungs_mutant: array<int> := new int[] [463]; var dist_mutant: int := 1; ///// FILLED IN WITNESS END ///// expect rungs_original.Length >= 1; ... // + 3 checks ///// FILLED IN PROOF BEFORE ORIGINAL CALL (empty) ///// var originalResult := AddMinimumRungs(rungs_original, dist_original); expect rungs_mutant.Length >= 1; ... // + 3 checks ///// FILLED IN PROOF BEFORE MUTANT CALL (empty) ///// var mutantResult := AddMinimumRungs_mutant(rungs_mutant, dist_mutant); ///// FILLED IN PROOF AFTER CALLS (empty) ///// print originalResult, " ", mutantResult; // 462 and 0 expect originalResult != mutantResult, "no divergence"; }

Consider a method 𝑀 with input domain 𝑋 and output domain 𝑌 , where 𝑌 represents both the returned values and the post-state of 𝑀’s modifies frame. The precondition is a predicate 𝑃 : 𝑋 → B, the postcondition is a predicate 𝑄 : 𝑋 × 𝑌 → B, and 𝑆 = (𝑃, 𝑄) is the specification. Dafny accepts 𝑀 only if it terminates whenever 𝑃 holds, so 𝑀 denotes a total function on the admissible inputs 𝑋𝑃 = { 𝑥 ∈ 𝑋 | 𝑃 (𝑥) }. Verifying 𝑀 against 𝑆, written 𝑀 |= 𝑆, establishes that 𝑄 (𝑥, 𝑀 (𝑥)) holds for all 𝑥 ∈ 𝑋𝑃 . We define strength through the set of outputs the specification admits for an input, 𝐴𝑆 (𝑥) = { 𝑦 ∈ 𝑌 | 𝑄 (𝑥, 𝑦) }. Definition 2.1 (Specification Strength). 𝑆 is strong if 𝑋𝑃 ≠ ∅ and |𝐴𝑆 (𝑥)| = 1 for every 𝑥 ∈ 𝑋𝑃 , weak if |𝐴𝑆 (𝑥)| > 1 for some 𝑥 ∈ 𝑋𝑃 , vacuous if 𝑋𝑃 = ∅, and infeasible if 𝐴𝑆 (𝑥) = ∅ for some 𝑥 ∈ 𝑋𝑃 .

DafnyCert

2.2

5

Certify Strong Approach

The Certify Strong approach checks Theorem 2.1 indirectly, by verifying a harness. The harness takes two copies 𝑥𝑜 and 𝑥𝑚 of the input, each required to satisfy 𝑃, calls 𝑀 once per copy to obtain 𝑦𝑜 and 𝑦𝑚 , and states 𝑦𝑜 = 𝑦𝑚 as its postcondition. For mutable inputs, the two copies have equivalent initial states but independent storage, so modifications made by the first call cannot affect the second. The comparison includes both returned values and the modified state. Method addPairwise_check in Listing 1 is an example of such a harness. Since Dafny reasons about a call only through the callee’s contract, the body of 𝑀 is opaque and the only available facts about the two results are 𝑄 (𝑥𝑜 , 𝑦𝑜 ) and 𝑄 (𝑥𝑚 , 𝑦𝑚 ). Verifying the harness, therefore, establishes that any two outputs the contract admits for one admissible input coincide, i.e., |𝐴𝑆 (𝑥)| ≤ 1. Written out, the obligation is: VC(𝑆) ≡ ∀𝑥𝑜 , 𝑥𝑚 ∈ 𝑋𝑃 . ∀𝑦𝑜 , 𝑦𝑚 ∈ 𝑌 . 𝑥𝑜 = 𝑥𝑚 ∧ 𝑄 (𝑥𝑜 , 𝑦𝑜 ) ∧ 𝑄 (𝑥𝑚 , 𝑦𝑚 ) =⇒ 𝑦𝑜 = 𝑦𝑚 . Definition 2.2 (Proof augmentation). A proof augmentation Π for 𝑆 consists of ghost Dafny code, which is used at verification time but never executed, yielding an augmented harness 𝐻 (𝑆, Π), with 𝐻 (𝑆, 𝜀) = 𝐻 (𝑆). Π is admissible when it leaves 𝑀, 𝑆, and 𝐻 (𝑆) untouched and introduces no unproved claims. Definition 2.3 (Certified strong). 𝑆 is certified strong when some admissible Π, by default the empty one, makes the solver report unsat for every obligation of 𝐻 (𝑆, Π), including ¬VC(𝑆), and when, in addition, ∃𝑀. 𝑀 |= 𝑆 and 𝑋𝑃 ≠ ∅ hold. From Theorem 2.1, vacuity is ruled out by the side condition 𝑋𝑃 ≠ ∅, and infeasibility by the side condition ∃𝑀. 𝑀 |= 𝑆. The certificate carries 𝑀 and verifies it, which establishes ∃𝑀. 𝑀 |= 𝑆. To detect vacuity, the validator appends assert false at the end of the harness and re-verifies it. If Dafny proves it, the assumptions reaching that point are contradictory (𝑋𝑃 = ∅) and the certificate is rejected. Although this check detects vacuous specifications, its failure does not guarantee nonvacuity due to solver incompleteness. We therefore assume that specifications certified strong have satisfiable preconditions. The augmentation Π allows a specification to be certified when its harness needs proof steps that the solver will not find on its own, as is the case of Listing 1. Proposition 2.4. If 𝑆 is certified strong then 𝑆 is strong. Proof. Since 𝐻 (𝑆, Π) verifies, its verification conditions VC(𝑆) hold. Consider any 𝑥 ∈ 𝑋𝑃 , and instantiate the condition with 𝑥𝑜 = 𝑥𝑚 = 𝑥. For any 𝑦𝑜 , 𝑦𝑚 ∈ 𝐴𝑆 (𝑥), the postcondition of the harness requires 𝑦𝑜 = 𝑦𝑚 . Hence 𝐴𝑆 (𝑥) contains at most one element, i.e., |𝐴𝑆 (𝑥)| ≤ 1. The two side conditions guarantee that 𝐴𝑆 (𝑥) is nonempty, and therefore |𝐴𝑆 (𝑥)| = 1. Thus 𝑆 is strong. □ Example. The method addPairwise from Listing 1 computes the pairwise sums of consecutive elements in a sequence n. The specification completely states the expected length of the output sequence (empty when n is also empty and |n| - 1 otherwise), and it also constrains the value of its elements (each element is the sum of the corresponding element in n and its immediate successor), fully capturing the method’s intended behavior. 1 (addPairwise_check in Listing 1). If it The Certify Strong approach generates the harness (○) 2 verifies (○), this shows that, for every admissible input, the method’s specification admits exactly one output, making it strong. Dafny may, nonetheless, fail to verify the harness even when the specification is strong. This happens in Listing 1’s example because, although the specification establishes equality between corresponding elements of the two output sequences, Dafny does not automatically infer from these element-wise equalities that the sequences themselves are equal.

6

Álvaro Silva, Isabel Amaral, Ruben Martins, and Alexandra Mendes

The harness, therefore, needs a proof augmentation Π. The ghost assert and forall statements in the PROOF region of Listing 1 establish sequence equality, enabling successful verification of the harness. 2.3

Certify Weak Approach

Definition 2.5 (Certified weak). 𝑆 is certified weak by a pair (𝑀 ′, 𝑥 0 ) when Dafny proves both 𝑀 |= 𝑆 and 𝑀 ′ |= 𝑆, a runtime check of 𝑃 establishes that the witness 𝑥 0 is admissible (𝑥 0 ∈ 𝑋𝑃 ), and running 𝑀 and 𝑀 ′ on 𝑥 0 produces different outputs. Listing 2 exemplifies such a certificate. The mutant must verify (𝑀 ′ |= 𝑆), and running the file exhibits the input 𝑥 0 on which the mutant and the original program diverge. Preconditions are checked at runtime because arbitrary witnesses often cannot be statically verified to fulfill them. For example, Dafny may exhaust its budget trying to prove that a list of 100 elements is sorted, whereas the compiled check evaluates this directly. We exclude from the dataset methods for which the compiler cannot convert the preconditions into a runtime check. We informally rely on the soundness of Dafny’s compiler and of its emitted precondition check (§5.5). Proposition 2.6. If 𝑆 is certified weak, then 𝑆 is weak. Proof. The runtime check of P gives 𝑥 0 ∈ 𝑋𝑃 . Verifying 𝑀 and 𝑀 ′ gives 𝑄 (𝑥 0, 𝑀 (𝑥 0 )) and 𝑄 (𝑥 0, 𝑀 ′ (𝑥 0 )), so both results lie in 𝐴𝑆 (𝑥 0 ), and, by compiler soundness, they correspond to the values produced by the runs, which differ. Hence |𝐴𝑆 (𝑥 0 )| > 1. □ Example. In Listing 2, the method AddMinimumRungs determines the minimum number of rungs that must be added to a ladder so that its top can be reached from the floor, given the heights of its existing rungs in rungs, and so that no step to the top exceeds dist. Though this method is labeled as strong in VeriEquivBench, the method’s postcondition only requires result to be non-negative, and says nothing about how many rungs should be added. Our pipeline classifies this specification as weak, and the certificate in Listing 2 was generated automatically by the Certify Weak approach. The Certify Weak approach first compiles 𝑀 to Python and uses a frontend we developed for the 3 Hypothesis [19] property-based testing library to sample inputs satisfying 𝑀’s precondition (○). For each sampled input, we record the output produced by the original implementation. We then 4 run MutDafny [2] (○), a mutation tool for Dafny that generates mutants and runs the verifier on 5 each of them. Mutants that verify are retained as alive mutants (○). To distinguish alternative implementations that are verified because the specification is weak from those that are simply equivalent to the original program, we execute both the original program and each alive mutant on the same sample of inputs and compare their outputs. The input selection 3 and the execution of the original method take place prior to mutation (○), as this only needs to 4 5 occur once. As MutDafny produces mutants (○), we run the alive ones (○) on the selected inputs 6 and compare their outputs with those of the original method (○). If we find a mutant whose output 7 differs from the original method’s, we build a candidate certificate and run Dafny on it (○). A divergence counts only once its certificate passes this check and, if it fails, the search moves on to the next divergent mutant. Once a certificate is successfully checked, we interrupt the mutation 4 ○). 6 and alive mutant execution stages (○, If every operator has been applied, or the time budget for mutation is exhausted without producing 8 a certificate, the method remains uncertified. The search also yields a mutation score (○): the fraction of generated mutants that failed to verify, which serves as a heuristic for classifying specifications. A high mutation score suggests that the specification constrains the code well, so it is heuristically strong. Otherwise, it is heuristically weak.

DafnyCert

7

In the certificate shown in Listing 2, the FILLED IN COUNTEREXAMPLE section records the mutant. It replaces the whole method body with the single assignment result := 0, an incorrect implementation that still verifies. The FILLED IN WITNESS section records the input on which the two outputs differ. In this case, the witness inputs were rungs := new int[][463] and dist := 1, for which the original method returns 462, whereas the mutant returns 0. 2.4

Certificate Validator

The validator component is what allows a certificate to be trusted without trusting whoever produced it. Both Certify Strong and Certify Weak approaches produce candidate certificates. The 9 evaluates a certificate regardless of its source. Thus, a bug in a certificate Certificate Validator (○) producer (e.g., DafnyCert, a human, or an LLM agent) can cause a certificate to be missed, but never an invalid one to be accepted. A certificate 𝐶 consists of the benchmark file plus generated code, in which only the FILLED IN marker regions may be written to. For a strong certificate, the regions form Π, which includes the top-level HELPERS region for lemmas and functions, and the proof-hint regions before each call to 𝑀 and after both calls (in Listing 1, only the proof-hint regions are filled). For a weak certificate, COUNTEREXAMPLE is the body of 𝑀 ′ (result := 0 in Listing 2), and WITNESS declares 𝑥 0 once per call. The HELPERS and proof-hint regions in Main follow the same structure as for strong certificates. The listings show each empty region as a single (empty) line. Let 𝑇 (𝑀, 𝑆) be the template regenerated from the benchmark source and blank(𝐶) be 𝐶 with its regions emptied. The validator accepts 𝐶 only if: • V1: Structure. The marker regions exist and are well-formed. • V2: Grounding. blank(𝐶) is byte-identical to 𝑇 (𝑀, 𝑆), so 𝑀, 𝑆, 𝐻 (𝑆), the contract of 𝑀 ′ , and the checks in Main are unchanged (i.e., in Listings 1 and 2, everything outside the FILLED IN blocks). • V3: No unsound constructs. No assume appears in a strong certificate, or in a weak certificate’s regions, and no region declares a lemma, method, or function taken on trust ({:axiom}, {:verify false}, or no body). Hence Π is admissible (Theorem 2.2) and 𝑀 ′ cannot verify by assumption. Weak regions also contain no expect, which could alter the run or skip a precondition check. • V4: Verification. dafny verify succeeds, establishing 𝑀 |= 𝑆 and 𝐻 (𝑆, Π) for a strong certificate, and 𝑀 |= 𝑆 and 𝑀 ′ |= 𝑆 for a weak one. • V5: Non-vacuity (strong only). The harness with assert false appended does not verify (see Theorem 2.3). • V6: Same input (weak only). 𝑀 and 𝑀 ′ receive inputs with equivalent initial states, using independent storage for mutable values. ([463] and 1 in Listing 2). • V7: Divergence (weak only). dafny run passes every runtime check of 𝑃, so 𝑥 0 ∈ 𝑋𝑃 , and confirms 𝑀 (𝑥 0 ) ≠ 𝑀 ′ (𝑥 0 ) (462 vs. 0 in Listing 2). The validator checks V1–V3 and V6 itself and delegates V4, V5, and V7 to Dafny. Under the non-vacuity assumption, V2–V4 establish Theorem 2.3, while V5 provides an additional check for vacuity. V2, V4, V6, and V7 discharge Theorem 2.5, so by Theorems 2.4 and 2.6 an accepted certificate implies its label. The trusted base is thus Dafny (its verifier and, for weak certificates, its compiler) and the validator (Section 5.5). 3

Automatically Certifying Strong Specifications

1 ○) 2 runs first on every method and tries to show that The certification of strong specifications (○– every implementation of 𝑆 agrees with 𝑀 on every admissible input, which it does by generating a

8

Álvaro Silva, Isabel Amaral, Ruben Martins, and Alexandra Mendes

1 that Dafny itself verifies (○). 2 harness 𝐻 (𝑆) (○) If verification fails, the method proceeds to the certification of weak specifications. The main challenge is constructing a harness such that Dafny has enough information to verify it automatically. Our design builds on the equivalence check introduced by VeriEquivBench [26], which we call VEB-Check, but uses a different encoding and supports a broader range of Dafny constructs.

3.1

A Robust Equivalence Harness

VEB-Check imposes a similar obligation with a single call. It havocs the outputs, assumes 𝑃 and 𝑄 on the havoced values, calls 𝑀 once, and asserts that the two agree. The logical content is the same, the difference is how many facts about the outputs must be restated by hand. A havoced output does not retain several facts that a normally returned value carries automatically, such as non-nullness or prior allocation, and the VEB-Check encoding does not restate all of them. This difference changes verification outcomes. For Dafny-Synthesis’s SquareArrayElements method (task_id_8, RQ1-GPT4), VEB-Check’s generator would produce the following harness: method SquareArrayElements_check(arr: array<int>) returns (res: array<int>) { res := *; assume arr != null; assume res != null; assume arr.Length == res.Length; assume forall i :: 0 <= i < arr.Length ==> res[i] == arr[i] * arr[i]; var val_0 := SquareArrayElements(arr); assert res.Length == val_0.Length; assert forall i :: 0 <= i < res.Length ==> res[i] == val_0[i]; // 1 error }

Despite the specification being strong, this harness does not verify. Since res is havoced, Dafny cannot establish that it was allocated before the call. Consequently, the callee’s frame does not preserve any information about it, and the assumptions on its contents are lost. Adding an assume allocated(res) would be enough to restore the missing allocation information and allow the harness to verify. In contracts without an explicit ensures res != null, havocing also drops the declared type’s non-nullness, leaving res.Length and res[i] ill-formed. Our harness avoids these problems by making two actual calls to the method, so 𝑄 reaches the check through the callee’s contract, and each result keeps its type, allocation, and frame information. The harness is also regular Dafny code without explicit assumes, which makes it easier to re-check. For methods that modify the heap, additional proof steps may be needed to establish the equivalence of the modified states. 3.2

Supporting a Broader Range of Dafny Programs

Beyond the harness encoding, we developed a generator that supports a broader range of Dafny programs. VEB-Check’s generator recovers method signatures using regular expressions, which can fail on nested parentheses and on identifiers that start with a keyword. Our generator instead extracts the method header from Dafny’s resolved AST. We also extend support for several Dafny constructs. VEB-Check hardcodes one-dimensional array accessors, treats the value type map as mutable, and does not resolve type synonyms. Our generator handles array rank explicitly, distinguishes value and reference types, and resolves type synonyms. VEB-Check also omits the equality check for an array that is both returned and modified, which can cause a weak specification to be classified as strong, although this did not occur in our evaluation. Finally, it does not model the receiver of an instance method, so modifications to receiver fields are not compared. Our generator explicitly represents the receiver and its modifies frame. Section 5.2 compares the certification rates of DafnyCert and VEB-Check.

DafnyCert

9

Table 1. The nine mutation operators we add to MutDafny’s catalogue Op.

Name

Mutation

Collection content. Weakness: a collection’s length is constrained, not its elements. Gap: only initializers change (CIR). CEU Collection Element Update Sets the first or last element of a collection to a default value CCC Collection Content Copy Assigns the contents of another collection to a collection CCU Collection Comprehension Update Assigns a default comprehension expression to a collection Collection order. Weakness: the elements are constrained, but not their order. Gap: no operator targets element order. CES Collection Element Swap Swaps the first two elements of an ordered collection CAS Sequence Concatenation Argument Swap Swaps the two operands of a sequence concatenation Arithmetic. Weakness: loose bounds, off-by-one results, unconstrained lengths. Gap: LVR mutates only literals. INC, DEC Arithmetic Expression Increment/Decrement Replaces a non-literal arithmetic expression 𝑒 with 𝑒 ± 1 ELR Expression-Collection Length Replacement Replaces an arithmetic expression with a collection’s length Whole method. Weakness: a trivial output satisfies 𝑄 (Listing 2). Gap: all operators are local. VSR Vacuous Stub Replacement Replaces the body with default assignments to the outputs

4

Automatically Certifying Weak Specifications

Certifying a specification as weak requires finding an alternative implementation 𝑀 ′ that verifies against the original specification 𝑆, together with an admissible input 𝑥 0 on which 𝑀 and 𝑀 ′ produce different outputs. To certify weak specifications, DafnyCert searches for 𝑀 ′ using program 3 ○). 8 mutations and for 𝑥 0 using property-based input generation (○– Two challenges arise. First, the search must find a mutant that both verifies and behaves differently, but MutDafny’s operators were not designed to expose specification weaknesses. Second, the search must be affordable. A method may admit hundreds of mutants, each of which must be verified, and restrictive preconditions make admissible inputs hard to generate. We address the first challenge with mutation operators aimed at specification weaknesses (Section 4.1). We address the second with input generation guided by the method’s preconditions (Section 4.2) and with a reduced set of mutation operators that keeps most of the witnesses while evaluating far fewer mutants (Section 4.3). 4.1

Generating Alternative Implementations

We use MutDafny [2] to generate candidate alternative implementations. This tool applies syntactic 4 mutation operators to the method under test, generating one implementation 𝑀 ′ per mutation (○), and verifies each against the original specification 𝑆. A mutant that verifies is therefore another 5 implementation of 𝑆 and is retained as an alive mutant (○). However, an alive mutant may still be behaviorally equivalent to the original implementation 𝑀, so verification alone is not sufficient to establish weakness. In Section 4.2, we search for an input that distinguishes 𝑀 and 𝑀 ′ . MutDafny defines 40 mutation operators, most being local perturbations of existing code. Thirty are adapted from operators implemented in mutation tools for other programming languages, while the remaining ten were derived from an analysis of implementation mistakes made by Dafny developers. To find the kinds of specification weakness MutDafny misses, two of the authors, each with three years of experience with Dafny, inspected the Dafny-Synthesis methods for which no alive mutant was found. For each method, they identified the behavior the specification leaves unconstrained and designed one operator whose mutant changes that behavior while still verifying. This yields the nine operators of Table 1, which target collection content, collection order, arithmetic expressions, and the method as a whole.

10

4.2

Álvaro Silva, Isabel Amaral, Ruben Martins, and Alexandra Mendes

Generating Witness Inputs

Given 𝑀 and an alive mutant 𝑀 ′ , we need to find an 𝑥 0 ∈ 𝑋𝑃 for which 𝑀 (𝑥 0 ) ≠ 𝑀 ′ (𝑥 0 ). We do this by running both methods on the same sample of inputs and comparing their outputs. The sample of inputs is generated using a frontend we built for the Hypothesis [19] property-based testing library for Python. To this end, both programs are compiled to Python by running dafny build –target:py. To ensure that candidate inputs satisfy 𝑀’s precondition 𝑃, we also compile a checked variant using Dafny’s –test-assumptions Externs option, which raises an exception whenever a precondition is violated, so that every accepted input satisfies 𝑃. The inputs are drawn 3 6 once against 𝑀 (○), and 𝑀 and 𝑀 ′ are both executed on them and their results compared (○). The sampler targets 200 admissible inputs per method. Our sampling pipeline has two stages. First, our Hypothesis frontend maps each Dafny type to a Hypothesis strategy, so that candidate inputs can be drawn for every supported type. A strategy exists for the primitive types bool, nat, int, real, char, and string. Collections, including seq, set, map, and up-to-four-dimensional arrays, are supported recursively over their element types. Tuples of any arity and nesting are also supported, as well as generic and directly recursive datatypes. Support is currently missing for multiset, recursive classes and traits, and mutually recursive datatypes. The frontend’s reliance on filtering (i.e., drawing candidate inputs without regard to 𝑃 and discarding those that the 𝑃 runtime check rejects) works well for relatively permissive preconditions, such as scalar bounds, but is ineffective for restrictive ones. For instance, an unguided draw has a very low probability of ever producing a strictly increasing array of positive integers, making it very difficult to find admissible inputs for methods with such a precondition and, as a result, to find a witness for them. To address this, a second component parses and identifies common precondition patterns in Dafny’s resolved AST and emits a Hypothesis composite strategy that incorporates these constraints when generating inputs, rather than filtering them out afterward. Recognized constraints are satisfied by construction, while all other cases fall back to filtering. Across the 3,031 methods with preconditions in the dataset, this component recognizes 88.3% of the 10,242 recorded precondition elements. Of those methods, 74.9% have every precondition element encoded into the sampling strategy, 99.0% have at least one, and only 30 are left entirely to filtering. Table 2 lists the supported precondition patterns and the Hypothesis constraints instantiated for each, which are then assembled into a @st.composite strategy. Parameters are drawn in an order that ensures every symbolic bound refers only to parameters that have already been drawn. The recognized constraints are those that can be built directly: bounds, memberships, distinctness, sortedness, row widths, column bounds, and calls to inlined helper predicates. Existential quantifiers, predicates that cannot be inlined, and recursive predicates remain out of scope. Listing 2’s preconditions require rungs to be a strictly increasing array of positive integers with at least one element, and dist to be a positive integer. If we blindly draw values and filter afterward, such an array almost never satisfies the precondition. The frontend instead emits a strategy that builds it directly: @st.composite def addminimumrungs_precondition_strategy(draw): rungs = draw(st.lists(st.integers(min_value=1), min_size=1, unique=True).map(sorted)) dist = draw(st.integers(min_value=1)) return (rungs, dist) 6 returns an input the checked variant accepted, and the certificate A successful witness search (○) records it so that anyone can reproduce the divergence. The certificate also emits 𝑃 as a check before each call, so running it re-tests admissibility.

DafnyCert

11

Table 2. The matched Dafny precondition clause patterns and how each of those patterns is converted into a Hypothesis strategy. p and q are parameters, k a literal, w a literal row width, a, b and c literal column indices, ⊲⊳ a comparison, f(q) an expression over already-drawn parameters, and lo and hi the accumulated minimum and maximum of same-direction bounds. Precondition Clause Shape

Hypothesis Constraint Rule

p ⊲⊳ 𝑘, p ⊲⊳ f(q)

st.integers(min_value=lo, max_value=hi)

p == a1 || ... || p == a𝑚

st.sampled_from([a1 ,..,a𝑚 ])

|p| ⊲⊳ k, |p| ⊲⊳ f(q)

st.lists(min_size=lo, max_size=hi)

forall i, j :: 0 <= i < j < |p| ==> p[i] != p[j]

st.lists(unique=True)

forall i :: p[i] ⊲⊳ p[i+1], forall i, j :: i < j ==> p[i] ⊲⊳ p[j]

st.lists(...).map(sorted(reverse=rev)), rev is True or False depending on the ⊲⊳ direction

forall i :: 0 <= i < |p| ==> p[i] ⊲⊳ k

for each p[i], p[i] = st.integers(min_value=lo,

forall i :: 0 <= i < |p| ==> p[i] == a1 || ... || p[i] == a𝑚

for each p[i], p[i] = st.sampled_from([a1 ,..,a𝑚 ])

p[k] == f(q)

generates p, then sets p[k] = f(q)

forall i :: 0 <= i < |p| ==> |p[i]| == w

st.lists(st.tuples(st.integers(), st.integers(), st.integers()).map(list), min_size=lo, max_size=hi) # w == 3

forall i :: 0 <= i < |p| ==> p[i][c] ⊲⊳ k

st.tuples(st.integers(), st.integers(min_value=lo, max_value=hi), st.integers()).map(list) # c == 1

forall i, j :: p[i][j] ⊲⊳ k

st.lists(st.lists( st.integers(min_value=lo, max_value=hi))) # one st.lists per dimension

max_value=hi)

As Section 2.3 describes, a runtime disagreement becomes a certificate only once the candidate file passes dafny verify and dafny run. Otherwise, the search moves on to the next divergent 8 mutant, and a method with no certificate keeps only its mutation score (○). 4.3

Reducing the Mutation Search Space

Generating and verifying every mutant is expensive [2]. Moreover, mutation operators often overlap in the weaknesses they expose. We therefore select a smaller set of operators that preserves witness-finding coverage while minimizing the number of mutants that must be verified. For each operator, we define its coverage set as the set of methods for which at least one mutant generated by it both verifies and yields a witness. We use these coverage sets to select a minimumcost subset of operators by formulating the selection as a minimum-cost partial set cover [9], which minimizes cost under a coverage floor. We solve this optimization over a sample of our dataset, and then apply the resulting subset to the full dataset. For each operator 𝑜, we introduce one binary decision variable 𝑧𝑜 , set to 1 when operator 𝑜 is kept and 0 when it is dropped, and define 𝐶𝑜 as the total number of mutants generated by 𝑜 across the sample, i.e., the cost of keeping 𝑜. The coverage sets are represented by 𝐸𝑜𝑚 ∈ {0, 1}, which, for each method 𝑚 in our sample that is covered by the full operator set, records whether operator 𝑜 is capable of producing an alive mutant and witness for 𝑚. For each method 𝑚, we also introduce a

12

Álvaro Silva, Isabel Amaral, Ruben Martins, and Alexandra Mendes

binary variable 𝑂𝑚 ∈ {0, 1} to indicate whether it is covered by the selected Í operators. Our goal is to minimize the total number of mutants generated by the kept operators, 𝑜 𝐶𝑜 𝑧𝑜 , while achieving a coverage level of 𝑝 among the 𝑁 methods covered by the full operator set: ∑︁ ∑︁ ∑︁ min 𝐶𝑜 𝑧𝑜 s.t. 𝑂𝑚 ≤ 𝑧𝑜 ∀𝑚, 𝑂𝑚 ≥ 𝑝 · 𝑁 , 𝑂𝑚 , 𝑧𝑜 ∈ {0, 1}, 𝑜

𝑜 : 𝐸𝑜𝑚 =1

𝑚

The first constraint forces 𝑂𝑚 = 0 when no kept operator covers method 𝑚. Since the solver may also set 𝑂𝑚 = 0 for a covered method once Í the floor is met, we compute the reported coverage from the kept operators 𝑧𝑜 rather than from 𝑚 𝑂𝑚 . This does not change the optimum. Setting 𝑝 = 1 requires the selected operators to cover every method in the sample, which corresponds to the standard minimum-cost set cover problem [12]. As an ablation, we sweep 𝑝 from 0.5 to 1 (Section 5.4). Because 𝑝 is only a floor, a solution may cover more methods than it requires, so Table 6 reports both the target 𝑝 and the coverage obtained. To measure the coverage sets 𝐸𝑜𝑚 , we must evaluate all operators rather than stop at the first certificate. We therefore run every operator on each method in the Selection Set, without early stopping and with an extended per-method budget. The Selection Set is a random sample of 491 VeriEquivBench methods (Section 5.4). With this data, operator selection is performed and the resulting operator set is evaluated on methods that the selection never saw (Transfer Set). We deploy the set selected at 𝑝 = 1. 5

Evaluation

We evaluate DafnyCert on a dataset of 3,910 Dafny methods from Dafny-Synthesis [21] and VeriEquivBench [26]. Our evaluation examines the effectiveness of automatic certification, the agreement between certified and existing benchmark labels, and the trade-offs involved in generating weakness certificates. We organize our evaluation around the following research questions: RQ1: How effectively does DafnyCert automatically certify specifications as strong or weak? RQ2: How do the certified labels produced by DafnyCert compare with those provided by existing benchmarks? RQ3: How do the strategies used to generate weakness certificates affect certification effectiveness and computational cost? Figure 2 shows the experiments we run, the data each one runs on, and the research questions that use its results. Arrows show what one experiment passes to the next. The dataset run E5 uses the operator set that E2 selects, and the methods it leaves uncertified go to E6. Each paragraph heading names the experiments it reports. 5.1

Dataset Construction and Experimental Setup

Datasets. Dafny-Synthesis [21] synthesizes Dafny methods for MBPP-derived programming tasks using GPT-4 and PaLM-2 under several prompting strategies. Each file contains a single method, and its specification is labeled by human annotators according to whether it captures the intended behavior of the corresponding natural-language task. VeriEquivBench [26] translates LeetCode problems into Dafny and may include multiple methods in a single file. Its labels are assigned at the file level, with an LLM prompted to generate one strong and one weak specification for each problem. The corresponding label therefore applies to every method in the file. Labels. The labels provided by both benchmarks are extrinsic, in the sense that they assess whether a specification captures the intended behavior described by the corresponding natural-language task. In contrast, our certified labels are intrinsic, since they depend only on the specification

DafnyCert

13 on the Selection Set RQ3

Selection Set 491 methods

sample

E1 All operators, no early stop

RQ3

witnesses

on the whole dataset RQ1 RQ2

Dataset 3,910 methods

RQ3

E2 Cheapest operator cover

selected set

E5 DafnyCert sweep

certificates 340 uncertified

E6 LLM agent closes residue

RQ2

E7 Certified vs. benchmark labels

labels

88 weak→strong

labels RQ3

VeriEquivBench

System performance Label changes RQ3 Ablation studies RQ2

RQ1 RQ2 RQ3

filter

Dafny-Synthesis,

RQ1

selected set RQ1 RQ2 RQ3

E4 Baselines VEB-Check, ProofPulse

E3 All vs. selected operators

RQ3

E8 Inputs with vs. without guidance

RQ2

E10 Manual review of 10 samples

E9 Recall on Transfer Set

Fig. 2. The experiments E1–E10 of the evaluation. Table 3. Dataset certified classification.

Table 4. Relabellings by direction.

Methods

Strong

Weak

Population

VeriEquivBench Selection Set Transfer Set Dafny-Synthesis

3,692 491 3,201 218

420 60 360 167

3,272 431 2,841 51

VeriEquivBench (all) single-method files Dafny-Synthesis

Dataset

3,910

587

3,323

str.→weak weak→str. changed 315 252 19

303 88 1

618 340 20

itself and characterize whether it admits more than one observable behavior, independently of the natural-language description. These notions are related but not equivalent. For tasks with a uniquely determined intended behavior, a specification that we certify as weak cannot fully capture that behavior, since its certificate exhibits two implementations that satisfy the same specification but produce different outputs on the same admissible input. Conversely, a specification that we certify as strong may still uniquely characterize behavior that does not match the natural-language intent. We account for this distinction when analyzing disagreements with the benchmark labels in RQ2. Dataset construction. We restrict the dataset to methods for which certificates can potentially be generated and validated. Overall, this filtering excludes 2,880 methods, with by far the largest category consisting of 2,612 methods which are not verified by Dafny. The remaining exclusions include files that do not compile, specifications containing untrusted constructs, methods without observable behavior, unsupported self-referential reference types, specifications labeled wrong in Dafny-Synthesis because their implementations are unrelated to the natural-language descriptions, and a small number of cases that could not be executed within the available resources. The resulting dataset contains 3,910 methods across 2,608 files, including 3,692 methods from VeriEquivBench and 218 from Dafny-Synthesis. After completing the certification process, 587 specifications are certified strong and 3,323 are certified weak, as summarized in Table 3. The table also shows the Selection Set, the subset of VeriEquivBench used to select mutation operators, and the Transfer Set, the rest of VeriEquivBench, on which we measure how that selection generalizes (Section 5.4).

14

Álvaro Silva, Isabel Amaral, Ruben Martins, and Alexandra Mendes

Table 5. Comparison between approaches that classify the strength of specifications over the certified dataset. weak System

VEB-Check ProofPulse DafnyCert

strong

classified

MCC

Cert.

Heur.

Cert.

Heur.

TP

FP

TN

FN

Unk. (FP, FN)

all

clean

CPU (h)

0 0

3,195 3,040

453 0

0 805

3,087 2,873

108 167

453 412

0 393

26, 236 8, 57

0.6569 0.4881

0.8837 0.5228

2.1 4.2

3,055

292

515

32

3,286

61

526

21

0, 16

0.9004

0.9226

58.0

Experimental Setup. All experiments were conducted on a workstation with a 16-core Intel Core Ultra 9 285H processor and 30 GiB of RAM, running Linux 6.18. We use Dafny 4.11.1 with Z3 4.12.1 inside the project’s container image. Experiments are run with up to 12 methods in parallel. Unless otherwise stated, reported execution times correspond to the sum of the elapsed time across individual methods rather than wall-clock time. Because the weakness search has a time budget per method and generates its inputs randomly, rerunning DafnyCert may produce slightly different results. The harness and validator have no wall-clock limit and rely only on Z3’s deterministic resource limit (250M units per assertion batch, the same for the harness, the vacuity probe, and the validator). The weakness search has a budget of 300 s per method, with only 97 of the 3,910 methods timing out. 5.2

RQ1: How effectively does DafnyCert automatically certify specifications as strong or weak?

Automatic certification (E5). DafnyCert automatically produces certificates for 3,570 of the 3,910 methods in our dataset (91.3%). Of the 587 specifications ultimately certified strong, 515 (87.7%) are certified automatically by DafnyCert. Of the 3,323 specifications ultimately certified weak, 3,055 (91.9%) are certified automatically by DafnyCert. The remaining 340 methods require additional effort to construct a certificate (E6), as discussed in Section 6. Comparison with existing approaches (E4). We compare DafnyCert with VEB-Check [26] and ProofPulse [28], two existing approaches for assessing specification strength. VEB-Check attempts to verify that a specification is strong by performing an equivalence check against the reference implementation. A successful check provides evidence that the specification is strong, whereas a failed check does not imply that the specification is weak. ProofPulse instead classifies specifications using a heuristic approach based on proof coverage and does not produce a certificate of strength or weakness under our definition. In contrast, DafnyCert produces independently checkable certificates for both weak and strong specifications. Table 5 summarizes the classifications produced by the three approaches, distinguishing those backed by a certificate (Cert.) from heuristic classifications (Heur.) and cases for which no classification is returned (Unk., divided into those that count as false positives and false negatives). A false positive (FP) is a specification classified as weak but certified strong, whereas a false negative (FN) is classified as strong but certified weak. Methods without a classification are counted as FNs if their certified label is weak and as FPs if their certified label is strong. Both are reported in the Unk. column. VEB-Check provides evidence-backed strong classifications for 453 methods, while its remaining classifications are heuristic, i.e., if a specification is not proven to be strong, it is considered weak by default. ProofPulse provides only heuristic classifications. In contrast, DafnyCert produces certificates for 3,570 methods (91.3%). For methods where no certificate is found, DafnyCert falls back on the mutation score, using a threshold 𝜏 = 1 to classify a specification as strong when its score is at least 𝜏 and weak otherwise. In other words, the presence of any alive

DafnyCert

15

mutant causes the specification to be classified as weak. This is the most conservative and easily defensible threshold, since if the mutation tool could guarantee that it never produces equivalent mutants, finding another program that verifies would be sufficient to prove that the specification is weak. This produces heuristic classifications for 324 additional methods. DafnyCert returns no classification for the remaining 16 methods (the Unk. column of Table 5), all of which are ultimately certified weak. For 9 of them, the input generator fails before any mutant is run, because the Hypothesis strategy built from the preconditions is unsatisfiable or impractical, e.g., a recognized lower bound exceeds the default value range, or a length constraint demands a list with tens of thousands of elements. For the others, MutDafny generates no mutant to verify, so there is neither a certificate nor a mutation score to classify by. MCC(all) counts all of them as misclassifications. We analyze the accuracy of these classifications against the certified labels below. Producing certificates requires additional computation, shown in the last column of Table 5 (Section 5.1). DafnyCert uses 58.0 hours of summed per-method CPU time, compared with 2.1 hours for VEB-Check and 4.2 hours for ProofPulse. Most of this time is spent on the methods that end up weak. The 515 methods proved strong take 0.3 hours in total (median 2.6 s per method), and the 3,055 certified weak take 42.1 hours (median 35.0 s), most of it spent verifying mutants. The 340 methods left uncertified account for 15.6 hours, or 26.8% of the total execution time. Of these, 97 exhaust the per-method search budget.

Classification accuracy (E4–E6). We use the completed certified dataset as ground truth to evaluate the classifications produced by DafnyCert, VEB-Check, and ProofPulse. The right-hand side of Table 5 reports the resulting confusion matrices and Matthews correlation coefficient (MCC), the correlation between predicted and certified labels, which ranges from -1 (all wrong) through 0 (chance) to 1 (all correct) and, unlike accuracy, is not inflated by the dominance of weak specifications in our dataset. We report MCC over the complete dataset, where unanswered cases are treated as incorrect, and over the subset of 3,570 methods for which all three approaches return a classification (MCC(all) and MCC(clean) in Table 5). DafnyCert achieves an MCC of 0.9004 over the complete dataset, substantially higher than VEBCheck (0.6569) and ProofPulse (0.4881). When considering only methods for which all approaches return a classification, DafnyCert reaches an MCC of 0.9226, compared with 0.8837 for VEB-Check and 0.5228 for ProofPulse. Thus, the additional evidence produced by DafnyCert also results in more accurate classifications. Figure 3 shows what the mutation-score fallback contributes. On the 324 methods that DafnyCert scores but does not certify, the scores of strong and weak specifications overlap. Equivalent mutants keep 61 of the 72 strong specifications below a score of 100%, so 𝜏 = 1 classifies almost all of them as weak, and 21 weak specifications reach 100% because no operator produces a mutant that verifies. On these methods, the score therefore reaches an MCC of only 0.0968 at 𝜏 = 1. A threshold of 83% would raise it to 0.6955 (AUC 0.8725), but that threshold is tuned on the certified labels themselves. We keep 𝜏 = 1, which needs no tuning, and report heuristic classifications separately from certified ones.

DafnyCert automatically certifies 91.3% of the dataset. Automatic certification is more effective for weak specifications, reaching 91.9%, than for strong specifications, reaching 87.7%. Scored against the completed ground truth, its classifications reach an MCC of 0.9004, compared with 0.6569 for VEB-Check and 0.4881 for ProofPulse.

16

Álvaro Silva, Isabel Amaral, Ruben Martins, and Alexandra Mendes (a) Uncertified methods

40 30 20 10 0

1.0

MCC on these methods

certified weak (252) certified strong (72)

50

methods

τ=1

(b) Score as a classifier

0.8

best: 83%, MCC 0.70

0.6 0.4 0.2 deployed: 100%, MCC 0.10

0.0 0

20

40

60

80

mutation score (%)

100

0

25

50

75

100

threshold on the mutation score (%)

Fig. 3. The mutation score as a fallback classifier, on the 324 methods that DafnyCert scores but does not certify. (a) Score distribution by certified label; methods left of the dashed line are classified weak under 𝜏 = 1. (b) MCC of the rule “weak iff score < threshold” on these methods, for every threshold.

5.3

RQ2: How do the certified labels produced by DafnyCert compare with those provided by existing benchmarks?

Disagreements with benchmark labels (E7). The certified labels disagree with the labels provided by the source benchmarks for 638 of the 3,910 methods in our dataset (16.3%). As shown in Table 4, this includes 618 of the 3,692 VeriEquivBench methods (16.7%) and 20 of the 218 Dafny-Synthesis methods (9.2%). Interpreting the VeriEquivBench disagreements requires some care because its labels are assigned at the file level, whereas our certificates classify individual methods. Of the 3,692 VeriEquivBench methods, 2,158 belong to files containing multiple methods and therefore inherit the same benchmark label. In particular, when a file is labeled weak, every specification in that file is marked as weak, even though some of those specifications may be strong under our definition. To avoid this mismatch, we restrict this analysis to the 1,534 VeriEquivBench files containing a single method. Among these files, 252 of the 359 specifications labeled strong (70.2%) are certified weak, whereas 88 of the 1,175 specifications labeled weak (7.5%) are certified strong. In the case of the Dafny-Synthesis benchmark, labels are human judgments over each method. Of the 20 disagreements, 19 correspond to specifications labeled strong that we certify weak, while only one corresponds to a specification labeled weak that we certify strong. The two disagreement directions have different interpretations, as discussed in Section 5.1. A strong→weak disagreement provides definitive evidence that the specification admits multiple observable behaviors despite being labeled strong by the benchmark. Moreover, the weakness certificate includes a concrete alternative implementation and input witnessing this ambiguity. For tasks whose natural-language description determines a unique intended behavior, such a witness is sufficient to establish that the specification is weaker than intended and that the benchmark’s strong label is incorrect. A weak→strong disagreement is less direct. The specification admits a unique behavior, but that behavior may still differ from the one described by the natural-language task. Resolving such cases therefore requires manual comparison with the task description. Dafny-Synthesis contains one weak→strong disagreement. Manual inspection confirms that the specification determines a unique behavior, as indicated by our certificate, but that this behavior does not match the natural-language description. Thus, in this case, the original weak label remains appropriate with respect to the intended task, even though the specification is strong in the behavioral sense measured by DafnyCert.

DafnyCert

17

Review of sampled VeriEquivBench disagreements (E10). VeriEquivBench has too many weak→strong disagreements to inspect them all, so we inspect a random sample of 10 of its 88 single-method cases. Two authors independently compared each specification with the natural-language description of its task. They agreed on all 10 methods, and in all 10 the specification matches the description. In every sampled case, the benchmark’s weak label is therefore wrong, and the certified strong label is correct. The way VeriEquivBench builds its labels explains this outcome. For each task, an LLM first translates the description directly into a strong specification, which is not required to verify. In a second step, the LLM receives that specification, the description, and a reference Python solution, and writes verified Dafny code whose specification is labeled weak. The label therefore records which step produced a specification, not an assessment of the specification itself. In 4 of the 10 sampled cases, the weak specification has the same postconditions as the task’s strong one. In 5 of the others, the strong specification has no postcondition at all, so the specification labeled weak is the stronger of the two. The sampled methods, their certificates, task descriptions, and both reviewers’ answers are part of the replication package. Our certified labels reveal substantial errors among specifications labeled strong in both LLMand human-labeled benchmarks, highlighting the difficulty of assessing specification strength. Among single-method VeriEquivBench files, whose labels are LLM-generated, 70.2% of specifications labeled strong are certified weak. In Dafny-Synthesis, whose labels are assigned by human annotators, 19 specifications labeled as strong are also certified as being weak. In the other direction, the benchmark’s weak label was wrong for all 10 sampled VeriEquivBench specifications that we certify strong. 5.4

RQ3: How do the strategies used to generate weakness certificates affect certification effectiveness and computational cost?

DafnyCert uses two strategies to reduce the cost of finding certificates to show that a specification is weak, namely, guided input generation from method preconditions and a reduced set of mutation operators. We evaluate the contribution of each strategy and also measure the impact of the new nine mutation operators added to MutDafny. Effect of precondition guidance (E8). To isolate the effect of precondition guidance, we ran the pipeline’s input-generation step twice over the whole dataset. Once using the guided composite strategy of Table 2, and once using the plain per-type proposal. The guided proposal produces at least one input satisfying the precondition for 3,771 methods (96.4%), compared with 3,432 (87.8%) without guidance. In particular, 346 methods yield at least one admissible input only with guidance. The median fraction of accepted draws is 100.0% with guidance, compared with 11.8% without it, since the guided proposal usually satisfies the precondition by construction. Moreover, 3,512 methods reach the full 200-input target with guidance, compared with 2,942 without it. Consequently, without guidance, 346 methods would receive no witness search because no admissible input would be found for them. Mutation operator reduction (E1, E2). Evaluating every mutation operator is expensive because each generated mutant must be verified by Dafny. We therefore select a smaller operator set using the minimum-cost coverage formulation of Section 4.3. We perform operator selection on the Selection Set and measure how the selected set transfers on the Transfer Set (Section 5.1). Of the 431 specifications in the Selection Set that are ultimately certified weak, a version of DafnyCert that uses all operators without early stop finds witnesses for 404. This run also has three

18

Álvaro Silva, Isabel Amaral, Ruben Martins, and Alexandra Mendes

Table 6. The cheapest operator set reaching each target coverage 𝑝 on Selection Set (upper). Obtained 𝑝 is the coverage of Selection Set’s witness-bearing methods the set reaches, which can exceed the target. Certs. is the % of the ground truth certificates covered. Budget is the share of the 112,734 mutants the full catalogue generates on Selection Set. † is the target the dataset sweep ran at. Operators names the operators we added and counts the rest as MO, operators of the original MutDafny catalogue. Target 𝑝

Obtained 𝑝

Certs. %

Budget %

Ops

Operators

Selection — cheapest set reaching each target 𝑝 on Selection Set (404 witness-bearing of 431 certified weak) 1.000† 1.000 93.7 22.7 12 CAS, CES, INC, VSR + 8 MO 0.990 0.990 92.8 11.8 9 CAS, CCU, INC, VSR + 5 MO 0.950 0.950 89.1 4.5 8 CAS, CES, VSR + 5 MO 0.900 0.901 84.5 1.4 2 VSR + 1 MO 0.800 0.822 77.0 1.0 2 CES, VSR 0.500 0.733 68.7 0.6 1 VSR Added operators — cheapest set at 97.5% coverage, the highest the original operators reach with added 0.975 91.4 8.0 7 CAS, CCU, VSR + 4 MO original only 0.975 91.4 52.5 8 8 MO Transfer — the chosen set, scored against each dataset’s weak certificates Transfer Set — 91.6 — 12 of 2,841 weak, not fitted on at all Dafny-Synthesis — 98.0 — 12 of 51 weak, operators’ design dataset

times the deployed per-method budget, because it records every witness each mutant finds rather than stopping at the first. It is the record the operator selection is solved on, while the comparison of the two operator sets under the deployed budget and early stop is reported below (E3). Table 6 reports the minimum-cost operator sets obtained for different coverage targets. Requiring complete coverage of the 404 methods selects 12 operators. This set retains 100.0% of the witnesses found by the version that uses all operators while generating only 22.7% of its mutants. Effect of the operator reduction (E3). To isolate the effect of the operator reduction, we ran two experiments that differ only in the operator set, using the same 491 methods from the Selection Set and the configuration in which the pipeline is deployed, once with every operator and once with the selected set. The reduced set requires 9.5 h of summed per-method time, compared with 20.7 h for the unrestricted set, a 2.2× speedup. The mutation stage alone requires 6.4 h, compared with 16.0 h. Unexpectedly, the reduced experiment also finds more witnesses, 402 compared with 381. Since removing operators cannot increase the set of methods they can cover, this difference is due to the fixed per-method budget, since 96 methods exhaust their budget with the unrestricted set, compared with 17 with the reduced set. Per method, both experiments find witnesses for 377 methods. The reduced set finds 25 more, every one of them a method on which the unrestricted set exhausted its budget, and misses 4 that the unrestricted set finds, 2 of them because it exhausts its own budget. Transfer to the Transfer Set (E9). Table 6’s Certs. column gives, for each row, the fraction of a dataset’s weak certificates that the operator set recovers with a witness. The denominator is the set of methods that the dataset ultimately certifies as weak. The selected operators cover 93.7% of weak specifications in the Selection Set and find witnesses for 91.6% in the Transfer Set under the deployed configuration. This suggests that the selected operators generalize well to methods not used during selection. The Transfer Set is independent of the selection, because the selection saw only the Selection Set, and the nine operators added to MutDafny’s catalogue were designed

DafnyCert

19

by inspecting Dafny-Synthesis (Section 4). Dafny-Synthesis reaches 98.0%, but since the added operators were designed on this dataset, this figure does not show generalization. Contribution of the added operators (E1, E2). Four of our nine additions survive selection (Table 6) and make up a third of the operators used in the dataset sweep. They contribute in two ways: they reach methods that no operator of the original MutDafny catalogue reaches, and they reach the remaining methods with far fewer mutants. Coverage. We measure generalization on the Selection Set, since no added operator was designed on it. There, the original MutDafny catalogue alone finds a witness for 394 of the 404 witnessbearing methods (97.5%), so the additions are necessary for only 10 (2.5%). On Dafny-Synthesis, on which they were designed, they are necessary for 8 of the 50 weak Dafny-Synthesis methods (16.0%), almost all through CAS and CES. Judged by coverage alone, the additions therefore have a modest impact. Cost. The main benefit of the added operators is a lower cost. Without them, no set of operators covers more than 97.5% of the witness-bearing methods in the Selection Set, so the deployed selection at 𝑝 = 1 would have no solution. We therefore compare both catalogues at 97.5% coverage, the highest coverage they both reach (middle block of Table 6). The cheapest set of original operators needs 8 operators and 52.5% of all mutants. With the added operators, 7 operators and 8.0% of the mutants are enough to reach 97.5% coverage. The same coverage thus costs 6.52× fewer mutants. The original catalogue has no cheap operator that changes the contents of a collection. Its cheapest cover must therefore use broad operators such as EVR, ROR, and MRR, which mutate almost every method and so produce many mutants that must all be verified. Because verifying mutants dominates the running time (Section 5.2), this reduction matters more than the small gain in coverage. Guided input generation increases the fraction of methods for which admissible inputs are found from 87.8% to 96.4%. The selected 12 operators generate only 22.7% of the mutants on the Selection Set and find witnesses for 91.6% of weak specifications on the Transfer Set. They also reduce execution time by 2.2× on the Selection Set. The added operators make the 𝑝 = 1 cover feasible and cut the mutants needed at 97.5% coverage by 6.52×. 5.5

Threats to Validity

Trusted base. Certified labels rely on Dafny (verifier, Z3, and, for weak certificates, the compiler and its runtime precondition checks) and the validator, which checks (V1)–(V3) and (V6) itself. Certificate producers (DafnyCert, humans, and the LLM agent) are not trusted. We assume that 𝑀 is deterministic. Strength certificates assume that the precondition is satisfiable. The validator checks for vacuity (V5) and rejects certificates when Dafny detects it, but this check cannot rule out all vacuous cases. External validity. The dataset is the largest publicly available collection of labelled Dafny specifications, but it is not industrial code, since both sources are benchmark problems with self-contained methods and small signatures. Industrial Dafny has larger heap footprints and richer module structure, which we expect to make applying our approach harder in engineering terms. Unsupported constructs. Self-referential reference types are out of scope by construction and are filtered at dataset-creation time (Section 5.1). In addition, the witness search’s precondition pattern table is finite, and existentials over domains the compiler cannot enumerate are handled only in the common case. A precondition shape we do not model can leave a method uncertified, but it cannot produce a wrong certificate, as the validator step checks this.

20

6

Álvaro Silva, Isabel Amaral, Ruben Martins, and Alexandra Mendes

Ground Truth Completion and Failure Analysis

DafnyCert automatically produces certificates for 3,570 of the 3,910 methods in our dataset (91.3%), leaving 340 methods uncertified. These uncertified methods can, in principle, be certified manually. For a weak specification, one can provide an alternative implementation that still verifies against the original contract, together with an input on which the two implementations disagree. For strong specifications, one can give additional information to the harness such as auxiliary assertions, loop annotations, or lemmas that will help Dafny to verify that no alternative output is possible. In this section, we describe how we complete the ground truth for the remaining methods and then use the resulting certificates to analyze why DafnyCert failed to certify them.

6.1

Completing the Ground Truth

Manually constructing certificates for all 340 uncertified methods would require substantial effort. We therefore first solved a small number of cases manually to identify recurring strategies for constructing weakness witnesses and completing strength proofs. We then encoded these strategies in a detailed prompt (available in the replication package), together with 7 manually completed certificates as few-shot examples (4 dataset methods and three small illustrative programs that are not in the dataset), and used a Claude Code agent (version 2.1.277) running Claude Sonnet 5 to apply them to the remaining 336 methods. Since the solutions of the 4 dataset examples appear in the prompt, we closed those methods by hand and did not give them to the agent, which therefore closed the other 336 of the 340 uncertified methods. The LLM agent also had access to a script that generates the skeleton of a strength or weakness certificate, which it then completed with either the required proof information or a candidate alternative implementation and witness. The LLM agent is not part of the trusted base because every candidate certificate must pass the same validator used for DafnyCert’s certificates (Section 2.4). Therefore, the correctness of the resulting label depends on the certificate passing validation, rather than on whether it was produced automatically, manually, or by an LLM agent. The validator accepted certificates for all 336 methods processed by the LLM agent. The agent could invoke the validator itself and repair rejected candidates. Of the 336 certificates, 279 passed on the first validator attempt, and no method required more than 10 attempts. Per method, the agent performed a median of 10 actions, including reading the method, generating the certificate template, editing it, and invoking the validator. Together with the four methods closed by hand, this yields certificates for all 3,910 methods in the dataset. DafnyCert needs 58.0 hours of summed per-method time and produced certificates for 91.3% of the methods. Each method is certified independently and the only resource used is CPU, so this time divides almost evenly across processes, which is about 4.8 hours on the 12 processes of our machine. The LLM agent completed the remaining 336 methods in around 6.8 hours, a time that does not shrink as easily with more processes, because the agent is bound by the API’s rate limits and per-token cost rather than by local CPU, at a total cost of $90.09, or $0.27 per method. Restricting the LLM agent to methods that remain uncertified substantially reduces the cost of obtaining a complete ground truth. Extrapolating from the observed cost on the uncertified methods, applying the same LLM agent directly to all 3,910 methods would cost approximately $1,048 and take about 79 hours. In contrast, DafnyCert incurs no per-method LLM cost, and certifies the large majority of methods in substantially less time.

DafnyCert

21

Table 7. Reasons why DafnyCert fails to automatically certify the remaining 268 weak specifications. Reason

6.2

Methods

Input generator failed No mutants generated No admissible inputs found No divergence (< 50 admissible inputs) No divergence (≥ 50 admissible inputs)

9 7 107 49 96

Total

268

Weak Specifications Not Certified Automatically

Of the methods left uncertified by DafnyCert, 268 are ultimately certified weak. Table 7 summarizes the reasons why these methods were not certified automatically. For 16 methods, DafnyCert produces no heuristic classification because input generation fails for 9 methods and MutDafny generates no mutants for the remaining 7 (Section 5.2). For 107 methods, input generation succeeds but finds no admissible input within the available budget. A likely cause is a precondition shape not covered by the patterns in Table 2, such as an existential or a recursive predicate. In these cases, the generator falls back to filtering, which is unlikely to satisfy restrictive preconditions. For another 145 methods, the search finds admissible inputs but no divergence. We use 50 inputs as a threshold to distinguish limited input generation from more extensive sampling. Of these, 49 produce fewer than 50 admissible inputs. The remaining 96 produce at least 50 admissible inputs and alive mutants, but none of the sampled inputs exposes a divergence. This may indicate insufficient input coverage or mutants that are behaviorally equivalent to the original implementation. Overall, many of the remaining failures come from the difficulty of finding inputs that expose a behavioral difference between the original implementation and a mutant. This suggests moving from largely random sampling toward more targeted witness generation. Inputs could, for example, be directed toward branch conditions affected by a mutation or boundary values appearing in the specification. Similarly, mutants could be constructed using values admitted by the specification rather than relying only on fixed syntactic transformations. 6.3

Strong Specifications Not Certified Automatically

The remaining 72 methods are certified strong. For all of them, Dafny fails to verify the equivalence harness generated by DafnyCert. These failures occur quickly, with a median verification time of 3.7 seconds, suggesting that increasing the verification budget would not resolve them. Instead, the harnesses require additional proof information that Dafny cannot infer automatically. The completed certificates show a consistent pattern. The added proof information has a median size of 32 lines and at most 80 lines. Of the 72 certificates, 59 introduce a lemma, and every such lemma is recursive. In addition, 69 use intermediate assertions and 34 use additional loop annotations. These categories are not mutually exclusive. The dominant difficulty therefore appears to be proving properties that require inductive reasoning, for example over sequences, array indices, or recursive datatypes. These results suggest that improving the certification of strong specifications requires better proof synthesis rather than a larger verification timeout. In particular, automatically generating recursive lemmas, intermediate assertions, and loop annotations could allow DafnyCert to certify many of these specifications without additional proof construction.

22

Álvaro Silva, Isabel Amaral, Ruben Martins, and Alexandra Mendes

The failure analysis exposes different bottlenecks. Weak specifications are missed primarily because the search fails to find a suitable witness, whereas strong specifications are missed because their equivalence proofs require additional inductive reasoning. 7

Related Work

Judging specification strength. Clover [24] combines LLMs and formal verification to check consistency between code, specifications, and natural-language descriptions. Mirchev et al. [20] jointly refine code, specifications, and tests to improve their consistency. IronSpec [10] uses sanity checks, specification mutations, and proofs to identify specification bugs. In contrast, DafnyCert produces checkable certificates showing whether a specification uniquely determines program behavior. Endres et al. [5] and Lahiri [14] propose metrics for measuring the strength of LLM-generated specifications. Endres et al. [5] quantify completeness as the fraction of mutants that fail under the specification, using likely faulty LLM-generated implementations and filtering out equivalent mutants with a test suite. Any mutant that fails a test is guaranteed to be non-equivalent. Lahiri [14] simplifies this by mutating the outputs of the validation test suite. Verus-SpecGym [1] extends this framework to an agentic setting, evaluating generated Verus specifications against humanwritten test cases. These approaches rely on a test suite, which, in practice, is often missing in verification-aware contexts, and there are no guarantees that the test suites themselves are complete. MutDafny [2] generates mutants deterministically, flagging alive ones as hints of a potential specification weakness, without needing a test suite. However, it produces many equivalent mutants, requiring a lengthy manual analysis of the alive mutants to confirm the weaknesses. Le-Cong et al. [16] also use mutations to measure the completeness of Java Modeling Language (JML) specifications, but their completeness rate remains a heuristic rather than a definitive verdict. ProofPulse [28] inspects a correctness proof and classifies a specification as strong if every line of the implementation is used to prove the postcondition. However, this can be misleading, as a specification may admit divergent implementations even when every line of the proof is used. VEB-Check [26], the equivalence check of VeriEquivBench, determines if a specification is strong through an equivalence proof harness. Successful verification provides assurance that the specification is strong, but a failure does not necessarily indicate a weakness, as strong specifications may still fail the check. This approach inspired our strength check, which we improved to reduce the cases of non-verification for strong specifications. To distinguish genuinely weak specifications from strong ones for which the verifier cannot complete the proof, we complement the strength check with a weakness certification approach. This combination allows us to produce certificates in both directions, which can be re-checked independently using Dafny and our validator, without trusting the generation pipeline. Test generation for Dafny. Before building our Hypothesis frontend, we considered existing test generation options for Dafny. Dafny itself provides built-in test generation through DTest [6], which does not support array inputs and preconditions with nested quantifiers. Moreover, this tool only generates the minimum number of tests required to achieve program coverage, which may be insufficient to catch divergent implementations. DSpec2Test [22] improves this to allow the generation of multiple test cases per program path, but its test generation approach is guided by the specification, rather than by the implementation, and it still suffers from lack of support for some Dafny features. DafnyCBT [23] is another specification-based test generation tool, which relies on its own Dafny-to-SMT translation. We avoid solver-based generation primarily because of speed and reliability. Much like our sampling approach, the extracted test inputs have to satisfy preconditions, and the SMT calls needed to extract them are much slower than our constructive approach.

DafnyCert

23

Furthermore, Z3 is difficult to steer towards varied inputs and tends to return the simplest ones. The main drawback of both DSpec2Test and DafnyCBT is, however, that they generate tests from the specification alone. Therefore, they are not fit for our use-case, which is to test the specification itself. Our frontend follows the property-based testing tradition of QuickCheck [3] and Hypothesis [19], drawing inputs from generators built from the precondition. 8

Conclusion

A verified Dafny method is only as trustworthy as its specification. We presented DafnyCert, which replaces heuristic assessments of specification strength with independently checkable certificates. A strength certificate uses a verified equivalence harness to establish that a specification admits at most one observable behavior for each admissible input, while a weakness certificate provides a verified alternative implementation and an input on which the two implementations disagree. Applied to VeriEquivBench and Dafny-Synthesis, DafnyCert automatically certifies 91.3% of the 3,910 methods. Guided input generation and a reduced set of 12 mutation operators make weakness certification more efficient. The selected operators generate only 22.7% of the mutants on the Selection Set while finding witnesses for 91.6% of weak specifications on the held-out Transfer Set. Certificates for the remaining 340 methods also passed the same validator, providing recheckable certificates for all 3,910 methods. The certified labels disagree with the benchmarks’ original labels for 16.3% of the methods. Among single-method VeriEquivBench files, 70.2% of specifications labeled strong are certified weak, as are 19 specifications labeled strong in the human-annotated Dafny-Synthesis benchmark. These findings highlight the limitations of relying on human- or LLM-assigned strength labels without independently checkable evidence, particularly when such labels are used to evaluate specification generation techniques. The failure analysis identifies two main directions for improvement. Weakness certification is primarily limited by the difficulty of finding admissible inputs and behavioral divergence, motivating more targeted witness generation. Strength certification often requires additional inductive reasoning, motivating automated synthesis of lemmas and invariants. The certificate-based approach could also be extended to other verification-aware languages, providing independently checkable evidence of specification strength beyond Dafny. Data-Availability Statement DafnyCert and its replication package are open source under the MIT license and archived on Zenodo at https://zenodo.org/records/23326759. The archive contains a Docker image with everything needed to run DafnyCert and reproduce the results. Besides the image, the archive contains a reviewer guide (README.md), the prompt of the agent fallback (agent_prompts/), and the supplementary material (supplementary_material/). Acknowledgments Alexandra Mendes and Isabel Amaral were partially funded by National Funds through the FCT Fundação para a Ciência e a Tecnologia, I.P. (Portuguese Foundation for Science and Technology) within the project VeriFixer, with reference 2023.15557.PEX (DOI: 10.54499/2023.15557.PEX) and by an Amazon Research Award, Fall 2024. Ruben Martins was partially supported by the National Science Foundation (NSF) under Award CCF2427581 and DARPA Agreement FA8750-24-9-1000. Álvaro Silva was co-financed by National Funds through the FCT - Fundação para a Ciência e a Tecnologia, I.P. (Portuguese Foundation for Science and Technology) within the project VeriFixer,

24

Álvaro Silva, Isabel Amaral, Ruben Martins, and Alexandra Mendes

with reference 2023.15557.PEX (DOI: 10.54499/2023.15557.PEX), and Fundação para a Ciência e a Tecnologia (Portuguese Foundation for Science and Technology) through the Carnegie Mellon Portugal Program under the fellowship reference PRT/BD/155045/2024. References [1] Anmol Agarwal, Natalie Neamtu, Pranjal Aggarwal, Seungone Kim, Jannis Limperg, Cedric Flamant, Kanna Shimizu, Bryan Parno, and Sean Welleck. 2026. Verus-SpecGym: An Agentic Environment for Evaluating Specification Autoformalization. arXiv preprint arXiv:2605.26457 (2026). [2] Isabel Amaral, Alexandra Mendes, and José Campos. 2026. MutDafny: A Mutation-Based Approach to Assess Dafny Specifications. In Proceedings of the 2026 IEEE/ACM 48th International Conference on Software Engineering (ICSE ’26). Association for Computing Machinery, New York, NY, USA, 3573–3585. doi:10.1145/3744916.3787816 [3] Koen Claessen and John Hughes. 2000. QuickCheck: a lightweight tool for random testing of Haskell programs. In Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP ’00), Montreal, Canada, September 18-21, 2000, Martin Odersky and Philip Wadler (Eds.). ACM, 268–279. doi:10.1145/351240.351266 [4] Leonardo Mendonça de Moura and Nikolaj S. Bjørner. 2008. Z3: An Efficient SMT Solver. In Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings (Lecture Notes in Computer Science, Vol. 4963), C. R. Ramakrishnan and Jakob Rehof (Eds.). Springer, 337–340. doi:10.1007/978-3-540-78800-3_24 [5] Madeline Endres, Sarah Fakhoury, Saikat Chakraborty, and Shuvendu K. Lahiri. 2024. Can Large Language Models Transform Natural Language Intent into Formal Method Postconditions? Proc. ACM Softw. Eng. 1, FSE, Article 84 (July 2024), 24 pages. doi:10.1145/3660791 [6] Aleksandr Fedchin, Tyler Dean, Jeffrey S. Foster, Eric Mercer, Zvonimir Rakamaric, Giles Reger, Neha Rungta, Robin Salkeld, Lucas G. Wagner, and Cassidy Waldrip. 2023. A Toolkit for Automated Testing of Dafny. In NASA Formal Methods - 15th International Symposium, NFM 2023, Houston, TX, USA, May 16-18, 2023, Proceedings (Lecture Notes in Computer Science, Vol. 13903), Kristin Yvonne Rozier and Swarat Chaudhuri (Eds.). Springer, 397–413. doi:10.1007/9783-031-33170-1_24 [7] Jean-Christophe Filliâtre and Andrei Paskevich. 2013. Why3 - Where Programs Meet Provers. In Programming Languages and Systems - 22nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings (Lecture Notes in Computer Science, Vol. 7792), Matthias Felleisen and Philippa Gardner (Eds.). Springer, 125–128. doi:10.1007/978-3642-37036-6_8 [8] Pedro Fonseca, Kaiyuan Zhang, Xi Wang, and Arvind Krishnamurthy. 2017. An Empirical Study on the Correctness of Formally Verified Distributed Systems. In Proceedings of the Twelfth European Conference on Computer Systems, EuroSys 2017, Belgrade, Serbia, April 23-26, 2017, Gustavo Alonso, Ricardo Bianchini, and Marko Vukolic (Eds.). ACM, 328–343. doi:10.1145/3064176.3064183 [9] Rajiv Gandhi, Samir Khuller, and Aravind Srinivasan. 2004. Approximation algorithms for partial covering problems. J. Algorithms 53, 1 (2004), 55–84. doi:10.1016/J.JALGOR.2004.04.002 [10] Eli Goldweber, Weixin Yu, Seyed Armin Vakil-Ghahani, and Manos Kapritsos. 2024. IronSpec: Increasing the Reliability of Formal Specifications. In 18th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2024, Santa Clara, CA, USA, July 10-12, 2024, Ada Gavrilovska and Douglas B. Terry (Eds.). USENIX Association, 875–891. https://www.usenix.org/conference/osdi24/presentation/goldweber [11] Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jacob R. Lorch, Bryan Parno, Michael Lowell Roberts, Srinath T. V. Setty, and Brian Zill. 2015. IronFleet: proving practical distributed systems correct. In Proceedings of the 25th Symposium on Operating Systems Principles, SOSP 2015, Monterey, CA, USA, October 4-7, 2015, Ethan L. Miller and Steven Hand (Eds.). ACM, 1–17. doi:10.1145/2815400.2815428 [12] Richard M. Karp. 1972. Reducibility Among Combinatorial Problems. In Proceedings of a symposium on the Complexity of Computer Computations, held March 20-22, 1972, at the IBM Thomas J. Watson Research Center, Yorktown Heights, New York, USA (The IBM Research Symposia Series), Raymond E. Miller and James W. Thatcher (Eds.). Plenum Press, New York, 85–103. doi:10.1007/978-1-4684-2001-2_9 [13] Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David A. Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. 2009. seL4: formal verification of an OS kernel. In Proceedings of the 22nd ACM Symposium on Operating Systems Principles 2009, SOSP 2009, Big Sky, Montana, USA, October 11-14, 2009, Jeanna Neefe Matthews and Thomas E. Anderson (Eds.). ACM, 207–220. doi:10.1145/1629575.1629596

DafnyCert

25

[14] Shuvendu K. Lahiri. 2024. Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages. In 2024 Formal Methods in Computer-Aided Design (FMCAD). 142–147. doi:10.34727/2024/isbn.978-3-85448-065-5_19 [15] Andrea Lattuada, Travis Hance, Chanhee Cho, Matthias Brun, Isitha Subasinghe, Yi Zhou, Jon Howell, Bryan Parno, and Chris Hawblitzel. 2023. Verus: Verifying Rust Programs using Linear Ghost Types. Proc. ACM Program. Lang. 7, OOPSLA1 (2023), 286–315. doi:10.1145/3586037 [16] Thanh Le-Cong, Bach Le, and Toby Murray. 2025. Can LLMs Reason About Program Semantics? A Comprehensive Evaluation of LLMs on Formal Specification Inference. 21991–22014. doi:10.18653/v1/2025.acl-long.1068 [17] K. Rustan M. Leino. 2010. Dafny: An Automatic Program Verifier for Functional Correctness. In Logic for Programming, Artificial Intelligence, and Reasoning, Edmund M. Clarke and Andrei Voronkov (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 348–370. doi:10.1007/978-3-642-17511-4_20 [18] Xavier Leroy. 2009. Formal verification of a realistic compiler. Commun. ACM 52, 7 (2009), 107–115. doi:10.1145/ 1538788.1538814 [19] David Maciver and Zac Hatfield-Dodds. 2019. Hypothesis: A new approach to property-based testing. J. Open Source Softw. 4, 43 (2019), 1891. doi:10.21105/JOSS.01891 [20] Martin Mirchev, Andreea Costea, Abhishek Kr Singh, and Abhik Roychoudhury. 2024. Assured Automatic Programming via Large Language Models. CoRR abs/2410.18494 (2024). arXiv:2410.18494 doi:10.48550/ARXIV.2410.18494 [21] Md Rakib Hossain Misu, Cristina V. Lopes, Iris Ma, and James Noble. 2024. Towards AI-Assisted Synthesis of Verified Dafny Methods. Proc. ACM Softw. Eng. 1, FSE (2024), 812–835. doi:10.1145/3643763 [22] Sofia Vieira Pinto, Álvaro F. Silva, João Pascoal Faria, and Alexandra Mendes. 2026. DSpec2Test: Specification-Driven Test Generation in Dafny. arXiv:2609.29713 [cs.SE] doi:10.48550/arXiv.2609.29713 [23] Álvaro Silva, Isabel Amaral, João Pascoal Faria, and Alexandra Mendes. 2026. Improving Debugging in VerificationAware Languages Through Automated Fault Localization: A Case Study in Dafny. In 2026 IEEE 37th International Symposium on Software Reliability Engineering (ISSRE). IEEE. doi:10.48550/arXiv.2608.05399 [24] Chuyue Sun, Ying Sheng, Oded Padon, and Clark W. Barrett. 2024. Clover: Closed-Loop Verifiable Code Generation. In AI Verification - First International Symposium, SAIV 2024, Montreal, QC, Canada, July 22-23, 2024, Proceedings (Lecture Notes in Computer Science, Vol. 14846), Guy Avni, Mirco Giacobbe, Taylor T. Johnson, Guy Katz, Anna Lukina, Nina Narodytska, and Christian Schilling (Eds.). Springer, 134–155. doi:10.1007/978-3-031-65112-0_7 [25] Xuejun Yang, Yang Chen, Eric Eide, and John Regehr. 2011. Finding and understanding bugs in C compilers. In Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, San Jose, CA, USA, June 4-8, 2011, Mary W. Hall and David A. Padua (Eds.). ACM, 283–294. doi:10.1145/1993498.1993532 [26] Lingfei Zeng, Fengdi Che, Xuhan Huang, Fei Ye, Xu Xu, Binhang Yuan, and Jie Fu. 2026. VeriEquivBench: An Equivalence Score for Ground-Truth-Free Evaluation of Formally Verifiable Code. In International Conference on Learning Representations, C. Vondrick, B. Hariharan, C. Raffel, L. Pinto, D. Yang, and A. Faust (Eds.), Vol. 2026. 146015–146063. https://proceedings.iclr.cc/paper_files/paper/2026/file/ebfa4297cd6419f64efe86f657ba49d0-PaperConference.pdf [27] Jean Karim Zinzindohoué, Karthikeyan Bhargavan, Jonathan Protzenko, and Benjamin Beurdouche. 2017. HACL*: A Verified Modern Cryptographic Library. In Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS 2017, Dallas, TX, USA, October 30 - November 03, 2017, Bhavani Thuraisingham, David Evans, Tal Malkin, and Dongyan Xu (Eds.). ACM, 1789–1806. doi:10.1145/3133956.3134043 [28] Álvaro F. Silva, Ruben Martins, and Alexandra Mendes. 2026. ProofPulse: Interactive Proof Coverage Analysis for Dafny. arXiv:2608.30818 [cs.SE] doi:10.48550/arXiv.2608.30818

Related documents

• DafnyCert: Certifying Specification Strength in Dafny#1659130
• The Semantic Obligations of Strong Universal Claims: An Evoluist Theorem of Audit-Domain Completeness#690592
• Towards a framework for certification of reliable autonomous systems#285498
• Diversifying to Verify: When Task-Equivalent Programs Differ in Verifiability#361509
• An AI Approach to Verified Production Cryptographic Libraries#1387139