MutDafny: A Mutation-Based Approach to Assess Dafny Specifications

(authored by agents unless marked 🧑)

Audit: audited 2026-10-13 against the paper; rechecked Table 1 and Table 2 sums and percentages, Figures 2 and 3 values, operator list and restrictions, mining counts, audit counts, page references and quotations; changed five places (four unmarked inferences now marked, one audit step stated as not described by the paper, one attribution of the Endres et al. finding reworded); the Verus sketch of shared_elements has no body or semicolon and was left as marked a sketch because the Verus reference gives no support for a fix, so it is unchecked.

source: Isabel Amaral, Alexandra Mendes, José Campos, arXiv:2511.15403v2 (12 Apr 2026), 13 pages, no appendix. The PDF prints no page numbers; pages below are counted from the first page.

earlier note: distributed_verification_review_b/deep_7_evaluation.md, in its part on MutDafny, already records the dataset, the score definition, the aggregate counts of Table 1, the 77/157/50 audit and the four mutant classes. It does not give the operators and their restrictions, the way new operators were mined, the tool’s pipeline, the per-operator results, the steps of the survivor audit, a Verus form, or the inconsistencies listed near the end. Those are the content here; the shared facts are repeated only where a step needs them.

the idea and the main caveat

Change the code slightly, keep the specification, and run the verifier. “If a program with a mutant verifies, this may indicate a weakness in the specification.” (Abstract, p.1) The paper builds a Dafny plugin with 40 mutation operators and runs it on 794 files.

The caveat is the word “may”. In the hand audit, of 284 surviving mutants only 77 pointed at a real weakness, and those 77 came from five specifications (§6.3.1, p.10). So a surviving mutant is a lead to check, and the score is not a measure of specification quality by itself.

The paper’s example (Listing 1, p.1) is a method SharedElements(a, b) whose postcondition says every element of the result is in both arrays. Deleting the if block that adds elements makes it return an empty sequence, and it still verifies: “Although this program verifies, removing the if block in Lines 16 to 18 (an error a human could make or a mutation tool could insert) causes it to always return an empty list — an incorrect behavior that still satisfies the specification.” (§1, p.1) The repair is to turn ==> into <==> in the first ensures and add a loop invariant saying every earlier common element is already in res.

proved, measured, trusted

Nothing is proved. Measured: how many mutants each operator produces and how Dafny classifies them (Table 1), a per-file mutation score (Figure 2), a hand audit of 284 survivors from 24 files (Table 2), and run time (Figure 3). Trusted: Dafny 4.10.0 and Z3 4.12.6 as the oracle, with Dafny’s default 20-second limit (footnote 34, p.8); one person’s judgment in the audit (p.9); the authors’ consensus on which commits show a mistake (§4.1.3, p.6).

technique 1: mutate the implementation, hold the specification, classify by verifier outcome

What it is. Mutation testing with the formal specification in the place of the test suite.

When to use. After a function verifies, to ask whether its contract would have rejected a wrong implementation. It applies most to code whose specification was written by the same author or agent as the code.

How it is done (§5, p.8).

1. Start from a file that verifies. The study drops any file that does not: “We excluded any files that (a) had validity errors with our Dafny/Z3 version, (b) timed out, (c) had verification errors, and (d) verified nothing at all (e.g., Dafny program verifier finished with 0 verified, 0 errors)” (§6.1, p.8).
2. Apply one mutation operator at one location to get one mutant. Specifications are not touched: the paper uses “implementation or code to refer to Dafny’s code within method or function bodies” (footnote 2, p.1).
3. Run Dafny’s resolver, then the verifier, on the mutant.
4. Classify: “Mutants are classified according to the verification outcome — Alive (survived): the mutant verifies successfully against the original spec, hinting at a potential specification weakness; Killed: the mutant fails verification, … meaning that the spec successfully detected the inserted fault; Invalid: the mutant fails during Dafny’s resolution process (before verification), indicating a semantically incorrect program; Timed Out: the verifier could not determine an outcome within a set time limit” (§5, p.8; the sentence runs across the two columns).
5. Hand the alive mutants to a person (technique 6).

Verus form. Inference: mutate only executable Rust inside fn bodies; leave requires, ensures, spec fn bodies, proof fns, loop invariant and decreases clauses, and assert statements as they are. Rust’s type and borrow checking plays the part of Dafny’s resolver for the Invalid class. The paper’s example in Verus terms is a function with the weak contract

verus! {
// sketch, not machine-checked; body omitted
fn shared_elements(a: &Vec<i32>, b: &Vec<i32>) -> (result: Vec<i32>)
    ensures
        forall|x: i32| result@.contains(x) ==> a@.contains(x) && b@.contains(x),
}

for which a body that returns an empty Vec verifies; the strengthened contract uses <==> in place of ==>.

Inference, on what does not carry over cleanly: “killed” in the paper means any verification failure. In Verus a mutant can fail because a loop invariant, an intermediate assert, a decreases clause, or an arithmetic overflow check no longer holds, while the ensures would still be provable with different proof annotations. Such a kill says the proof is specific to the code, not that the contract excludes the mutant. The paper notes one instance of this for Dafny: “For instance, certain mutations (e.g., inserting a continue before a counter update) may prevent Dafny from verifying loop termination.” and “These can easily cause verification to fail simply due to the application context.” (§3.3.8, p.4) A Verus tool should record which obligation failed and count a kill for the contract only when it is an ensures of the mutated function or a requires at one of its call sites.

Evidence. Table 1 (p.10), all 40 operators, 794 files: 118,458 mutants generated; 76,517 killed (64.6%), 30,459 survived (25.7%), 10,996 invalid (9.3%), 486 timed out (0.4%). The four add to 118,458 and each percentage matches.

Where it fails. The paper says it in the introduction: “Nevertheless, an alive mutant may not always indicate the presence of a weak specification; i.e., the mutant might just be equivalent to the original program [13, 43, 55], meaning that, despite the change, its behavior remains the same as that of the original program.” (§1, p.2)

technique 2: choose operators from existing mutation tools by two applicability tests

What it is. A way to get a starting operator set for a verification language from tools for ordinary languages.

How it is done (§3, pp.2-5).

1. Pick the popular tools for the languages the target compiles to: Stryker.NET, Mull, Major, MuJava, PIT, StrykerJS, Go-Mutesting, Mutmut, MutPy (§3.1, p.3).
2. List their operators from papers, documentation and, for Mutmut, source code; group the ones that do the same thing (§3.2, p.3). Result: 147.
3. Keep an operator if it passes two tests: “We consider a mutation operator applicable to a Dafny program if (a) the Dafny programming language supports the operation performed by the operator, and (b) if it has the potential of leading to a valid program.” (§3, p.2)
4. Remove those that can only give equivalent mutants. “Of these, we identified 97 that can be applied to Dafny programs and 50 that cannot due to the syntax structure of Dafny 4.10.0.” Seven of the 97 always give equivalent mutants. “Finally, the 90 operators were narrowed down to 30 unique ones, as many reflected the same behavior.” (§3.3, p.3)
5. Record each operator’s restriction, so that mutants are not trivially rejected.

The 30 operators and their restrictions (§3.3, pp.3-5):

• AOR, arithmetic operator replacement: “In Dafny, this reflects in allowing free replacement between the +, −, and ∗ group of operators, and only allowing / to be replaced with % and vice-versa.” (§3.3.1, p.3) The reason given is that / and % need a proof that the divisor is not zero
• AOI, AOD: insert or delete unary minus
• ROR: swap among ==, !=, <, <=, >, >= freely
• BBR: replace a relational or conditional binary expression by true or false
• COR: swap && and ||; COI, COD: insert or delete ! on a boolean
• LOR, LOI, LOD: the same for bit-vector &, |, ^ and !; SOR: swap << and >>
• LVR: literal replacement (boolean complement; strings to empty or default; numbers incremented, decremented, negated, or set to 0, 1, −1)
• EVR: replace a primitive-typed expression by a literal
• MRR: replace a call to a non-void method by default values of its return types; MAP: replace a call by one of its arguments of the return type
• CIR: replace a collection initialization by the empty collection of that type, or a constructor call by null
• LSR: swap break and continue, or either with return in a void method; LBI: insert break at loop entry
• CBR: in a match, replace the default case body by the first other case body and the other bodies by the default body
• SDL: delete a statement; delete a whole block (a void method’s body, an if branch when there is no else, a case); delete a call to a void method; MNR: drop a method call but keep its receiver when types agree; delete a constant field’s initializer or a constructor body
• VDL: delete every use of a variable, with the adjoining operator; SLD: delete one bound of a sequence slice; ODL: delete every occurrence of an operator with one operand
• PRV: assign a different child-class object; THI, THD: insert or delete this where a parameter shadows a field; AMR, MMR: swap getters or setters of the same signature

Excluded, with reasons (§3.4, p.5): operators for syntax Dafny lacks (compound assignment, switch, exceptions, overloading); parent and child type swaps, which give invalid or equivalent mutants; static insertion and deletion, equivalent because only constants can be static.

Verus form. Inference: the same two tests applied to Rust keep most of the list. AOR, ROR, COR, COI, COD, BBR, LVR, EVR, MRR, MAP, CIR (to Vec::new()), LSR, LBI, CBR on match arms, SDL, SLD, bit and shift operators all exist in executable Rust. THI and THD do not apply, since Rust always writes self.; PRV has no class hierarchy to act on. AOR behaves differently: Verus checks machine-integer overflow, so replacing + by * will often be killed by an overflow obligation, not by the contract, which is the Verus counterpart of the paper’s divisor restriction.

Evidence. Per-operator outcomes for the 30 (Table 1, p.10): 96,785 mutants, 62,886 killed (65.0%), 23,635 survived (24.4%), 9,920 invalid (10.2%), 344 timeouts (0.4%). Inference: operators with a high invalid share are poor value, since invalid mutants are discarded from the score. Invalid shares: MAP 2,539 of 5,399 (47.0%), ODL 2,014 of 4,418 (45.6%), MRR 874 of 2,286 (38.2%), VDL 460 of 1,248 (36.9%). CBR almost always survives: 364 of 369 (98.6%). AMR, PRV and THD produced no mutants in 794 files.

technique 3: mine new operators from bug-fix commits

What it is. Read fixes in real projects backwards to learn which mistakes people make in this language.

How it is done (§4.1, p.6).

1. Collect repositories: the 120 behind DafnyBench minus 10 (no URL, unavailable, repeated, or a subset of another), plus the AWS encryption SDK and Dafny-EVM, giving 112.
2. Bug reports were nearly absent (108 of 112 repositories had none), so use commit messages: 12,308 commits.
3. Filter with git log and grep for the stems fix, correct, updat, chang. Result: 1,475 commits.
4. Ignore changes to specifications: “Since our goal is to mutate implementations, changes involving specifications were disregarded.” (§4.1.3, p.6)
5. Read each fix in reverse: “Given we aim to synthesize modifications, as mutation operators, that introduce mistakes to the code and not that fix the code, we analyzed the inverse of bugfix commits, i.e., bugfixes as bug-introducing.” (footnote 14, p.6)
6. Each of the three authors reads a third (about 491) and notes candidate changes; 270 commits (18.3%) are candidates.
7. Meet and decide by consensus: “Of the 270, 148 were accepted, and 122 were not (Section 4.3 describes some reasons for this).” (§4.1.3, p.6)
8. Reject changes that alone do not alter behavior (nat to int), changes forced by the Dafny 3 to 4 migration, and code improvements such as adding ghost (§4.3, pp.7-8).

The result is ten new operators and one extension (§4.2, pp.6-7):

• COR extended to ==>, <==, <==>
• VER: replace a variable reference by another in-scope variable of the same type
• FAR: replace a field access by another field of the same class and type, e.g. item.price * item.stock to item.price * item.price
• MCR: replace a call by a call to another method with the same signature; DCR: replace a datatype constructor by another of the same datatype with the same arguments
• MVR: replace a method call by a variable of the return type
• SAR: swap two arguments of the same type in one call
• TAR: replace a tuple index by another of the same element type
• CBE: replace an if statement by the body of one of its branches
• SWS: “We propose swapping a statement with the one directly above or below it.” (§4.2.6, p.7)
• SWV: swap the initializers of two variable declarations in the same scope

Verus form. The paper says nine of the ten could also be applied in other languages and one is tailored for Dafny, without naming which (§4.2, p.6). Inference: all ten have a Rust counterpart: VER, FAR on struct fields, MCR, DCR on enum variants, MVR, SAR, TAR on .0 and .1, CBE, SWS, SWV. The extended COR touches operators that in Verus exist only in specification code, so it does not apply to executable mutation. Repeating the mining on Verus projects is possible in principle; the paper found only 1,475 candidate commits across 112 Dafny repositories, and whether public Verus history is large enough is not known from this paper.

Evidence. Table 1 (p.10), the ten new operators: 21,673 mutants, 13,631 killed (62.9%), 6,824 survived (31.5%), 1,076 invalid (5.0%), 142 timeouts (0.7%). VER dominates with 11,904. Survival is highest for MCR (349 of 478, 73.0%) and SWS (2,194 of 3,671, 59.8%). In the audit, 5 of the 15 operators that exposed a weakness were new ones: VER 14 mutants, MVR 4, DCR 3, CBE 2, SWS 2 (Table 2, p.10).

Where it fails. Inference: keyword filtering finds only commits whose message says fix, so mistakes fixed silently are missed, and “updat” and “chang” probably admit many commits that fix nothing. The paper gives the count (1,205 of 1,475 were not candidates) but not this reason.

technique 4: an AST plugin between parser and verifier

What it is. The tool design. “MutDafny works at the level between the parser and verifier and consists of a two-phase pipeline: mutant generation and mutation analysis, illustrated in Figure 1.” (§5, p.8)

How it is done (§5, p.8; Figure 1, p.9).

1. A scanner walks the syntax tree and lists mutation targets. “Namely, for each target, MutDafny records the node’s position, the type of mutation operator to be used, and any additional arguments required to apply the mutation.”
2. Some targets need types, which exist only after resolution (AOI applies only to numeric expressions). So there are two scans, one before and one after resolution.
3. A mutator takes the unresolved tree, walks to one target, and edits it: change a node’s data, replace an expression or statement by a new node, or remove a node from its parent. One mutant per target.
4. Dafny resolves the mutant (rejecting invalid ones) and verifies it.
5. In the study, jobs were parallelized: one scanner job per file and operator, one mutator job per file (§6.1, p.8).

Verus form. Inference: the same two scans map onto Rust syntax (before types) and type-checked Rust (after types). The filter that Verus needs and Dafny’s plugin gets from the grammar is skipping everything in ghost mode: spec fn and proof fn bodies, proof blocks, and specification clauses.

Evidence. Figure 3 (p.11), per file, in seconds: total median 306.4, mean 1,331.6, max 156,669.8; mutation analysis median 162.7, mean 972.7; generation median 141.2, mean 358.9; plugin alone median 7.5, mean 20.9. The text gives the mean as 22 minutes and says half the files take between two and 13 minutes (§6.3.3, p.10). The plugin’s own work is about 5% of generation time; the rest is Dafny resolving each mutant (p.11). Hardware: a cluster node with 1GB of RAM and an Intel E5-2450 at 2.1GHz (§6.1, p.8).

Where it fails. Inference: cost grows with mutants per file (2.7 per line here, §6.3, p.9) times verification time. The longest file took about 43.5 hours (156,669.8 s).

technique 5: mutation score that leaves out invalid and timed-out mutants

What it is. The summary number. “Additionally, we compute the mutation score [26], i.e., the ratio of killed mutants to the total number of mutants, excluding invalid mutants, e.g., that introduce non-compiling changes, and time-out ones, which reflect an inconclusive result.” (§6.2, p.9)

How it is done. Per file: killed / (killed + alive). Report the distribution over files.

Evidence. Figure 2 (p.9): median 92.6%, mean 82.5%, standard deviation 22.7%. The text: “On average, the dataset’s specifications are able to kill 82% of the mutants.” (§6.3.1, p.9) The middle half of files lies between 76% and 96%.

Verus form. Inference: the same ratio, with two additions suggested by technique 1: split kills by the kind of obligation that failed, and report the count of functions with no ensures separately, since every mutant there survives or dies for reasons unrelated to that function’s contract. The paper gives the size of that group for Dafny: of 2,747 methods, functions and similar constructs, 1,403 have no postcondition and 1,044 have neither pre- nor postcondition (§6.1, p.8).

Where it fails. A high score does not show the specification matches intent, and the paper’s own audit found weak specifications in files of a dataset whose mean score is 82%.

technique 6: audit the survivors

What it is. The step that turns surviving mutants into findings.

How it is done (§6.3.1, pp.9-10).

1. Split survivors by where they sit. “From the 30,459 surviving mutants, 11,035 affect methods with post-conditions.” For the rest: “The remaining 19,424 can be weak due to a lack of specification in the mutated component, hint at a weakness in a component calling the mutated one, or be equivalent to the original program.” (§6.3.1, p.9)
2. Sample. The study took 24 random files and their 284 survivors in methods with postconditions (1,205 lines, 79 functions).
3. For each survivor decide between three outcomes: it hints at a weakness, it is equivalent to the original, or no conclusion. The paper gives these outcomes but not the criteria or procedure used to decide.
4. For a suspected weakness, strengthen the specification and re-run; the mutants should now be killed.
5. Report upstream.

Evidence. One person, eight hours, about 1.7 minutes per mutant. “Of the 284 analyzed mutants, 77 hinted at these weaknesses and were successfully killed upon strengthening the specifications, 157 were equivalent to the original program, and we could not draw meaningful conclusions from the remaining 50.” (§6.3.1, p.10) That is 27.1% useful, 55.3% equivalent, 17.6% unresolved. The 77 map to five specifications in five files: bst4copy (insert does not say the value was inserted), task_id_126 (the postcondition bounds each common divisor but does not fix the sum), and task_id_161, task_id_2, task_id_249 (results constrained to be a subset, so the empty result passes). Per file the revealing mutants were 25, 27, 12, 2 and 11 (Table 2, p.10). The operators that revealed most were EVR 15, VER 14, ROR 7, BBR 7, COR 6, MAP 6.

Verus form. Inference: steps 1 to 4 carry over unchanged, and step 4 is mechanical in Verus too: after the ensures is strengthened, the original must still verify and the listed mutants must fail on that ensures. Step 3 is where an agent would be used, and it is the step with the lowest yield: more than half of the audited survivors were equivalent.

Where it fails. The paper’s stated remedy for the cost is a usage pattern, not a mechanism: “In practice, we expect MutDafny to be used as a validation tool alongside development to incrementally validate new components rather than entire projects at once.” (§6.3.1, p.10) Its planned mechanism is coverage: “As future work, we aim to investigate the application of code coverage of Dafny specifications to minimize the number of generated mutants [28], i.e., if a particular code portion is not covered by any existing specification in the program, then no mutant in it can ever be killed.” (§7, p.11)

inconsistent figures and missing information

• two different averages. The mean per-file score is 82.5%. From Table 1’s totals the pooled score is 76,517 / (76,517 + 30,459) = 71.5%. The paper reports only the first. Inference: large files with many survivors weigh little in a per-file mean.
• “real-world”. The abstract speaks of “five weak real-world specifications”. Four of the five files are dafny-synthesis tasks, which the paper says “were generated by LLMs for a study [45]” (§6.3.1, p.9). Of those four, one had been reported by that study’s authors (Misu et al.) and two had previously been detected by Endres et al.; one was new. The fifth (bst4copy) could not be reported because its repository was gone.
• Table 2 has a row “UOI” with one mutant. No operator of that name is among the 40 or in Table 1. The text’s count of “10 of the existing and five of the newly proposed operators” (p.10) only works if UOI is counted as one of the existing ten.
• phase times. The text says: “The two phases of the mutation testing pipeline — generation and analysis — present similar average runtimes.” (§6.3.3, p.11) Figure 3’s means are 358.9 s and 972.7 s; only the medians (141.2 s and 162.7 s) are similar.
• new against old operators. A Wilcoxon test is reported as showing specifications kill mutants of the 30 old operators significantly more often than those of the 10 new ones (p.10). In pooled terms that is 62,886 / (62,886 + 23,635) = 72.7% against 13,631 / (13,631 + 6,824) = 66.6%. The paper reads this as a reason to want tailored operators; it does not show that the extra survivors of the new operators reveal weaknesses rather than equivalents.
• Table 1 prints the SWS timeout share as “13 (0. %)”; 13 / 3,671 is 0.4%.
• the dataset has 785 DafnyBench files of which 42 did not verify in the authors’ environment, so 743, plus 17 and 34 from the two industrial projects: 794. The audit’s 24 files are not broken down by source, and all five weak specifications are in DafnyBench files, so the study shows nothing about the AWS and Dafny-EVM specifications.
• not reported: how many of the 157 equivalent mutants each operator produced, and any agreement check on the audit, which one person did.

not to redo in VL

Inference:

• the survey of 147 operators from nine tools and the 40-operator list with restrictions are done and public; a Verus mutation tool can start from that list and only decide Rust applicability
• the finding that subset-style postconditions (==> where <==> was meant) let an empty result pass has now been found three times on the same benchmark, by this paper, by Misu et al. and by Endres et al.; it is a known pattern to test for directly, not a discovery to repeat
• open and worth doing: attributing kills to the contract or to proof annotations, automatic removal of equivalent mutants, and a measure of how often an agent can do the audit step correctly

threat to VL’s product

Inference: low as a competitor, since the tool is Dafny-only and stops at a list of survivors for a person to read. It is relevant as a standard that buyers may come to expect: a product selling agent-written verified Rust will be asked how it knows the specifications are not weak, and a mutation score is the obvious answer someone else can compute. The paper’s audit shows the answer is expensive to make trustworthy (1.7 minutes of expert time per survivor, 27% yield), which is the part a product could do better.

techniques for the catalog

• implementation mutation against a fixed specification: mutate code only, re-verify, and treat a mutant that still verifies as a lead to a weak contract
• four-way mutant classification: alive, killed, invalid before verification, timed out, with only the first two entering the score
• two-test operator applicability: keep an operator from another language if the target language supports the operation and the result can be a valid program, then drop always-equivalent ones
• operator restriction table: record per operator which replacements are allowed so mutants are not rejected for trivial reasons such as a missing nonzero-divisor proof
• reverse bug-fix mining: filter commit messages by fix-like stems, read each fix backwards as the mistake, and agree by consensus on new operators
• pre- and post-resolution target scanning: find syntactic targets before type resolution and type-dependent targets after it, then mutate the unresolved tree one target at a time
• per-file mutation score excluding invalid and timed-out mutants: killed over killed plus alive, reported as a distribution over files
• survivor audit restricted to functions with postconditions: sample, label each survivor weakness, equivalent or unclear, and confirm a weakness by strengthening the contract until the mutants die
• subset-postcondition check: where a result is specified only as contained in something, test whether the empty or unchanged result verifies
• incremental mutation during development: run mutation on each new component as it is written to keep the survivor list short

Last edited: 2026-10-13