一句话：提出 MutDafny 工具，用 40 个变异算子通过变异测试自动暴露 Dafny 形式规约的弱点。
在 Dafny 等验证感知语言中，规约与实现同样容易出错，规约缺陷会导致形式验证通过的程序偏离预期行为。本文提出 MutDafny，用变异测试揭示 Dafny 规约的弱点：向代码注入变异（故障），再依赖形式规约检测它们；若含变异体的程序仍能通过验证，则说明规约可能存在弱点。作者分析了主流工具的变异算子，筛选出适用于 Dafny 的部分，并从 GitHub 公开 Dafny 项目的缺陷修复提交中合成新算子，最终集成 40 个变异算子。在 794 个真实 Dafny 程序上评估了工具的有效性与效率，人工分析未被检测的变异体后确认了 5 个存在弱点的真实规约（平均每 241 行代码约 1 个）。
In verification-aware languages, such as Dafny, despite their critical role, specifications are as prone to errors as implementations. Flaws in specifications can result in formally verified programs that deviate from the intended behavior. In this paper, we explore the use of mutation testing to reveal weaknesses in formal specifications written in Dafny. We present MutDafny, a tool that increases the reliability of Dafny specifications by automatically signaling potential weaknesses. Using a mutation testing approach, we introduce faults (mutations) into the code and rely on formal specifications for detecting them. If a program with a mutant verifies, this may indicate a weakness in the specification. We extensively analyze mutation operators from popular tools, identifying the ones applicable to Dafny. In addition, we synthesize new operators tailored for the language from bugfix commits in publicly available Dafny projects on GitHub. Drawing from both, we equipped our tool with a total of 40 mutation operators. We evaluate MutDafny’s effectiveness and efficiency on a dataset of 794 real-world Dafny programs, and manually analyze a subset of the resulting undetected mutants, identifying five weak real-world specifications (on average, one at every 241 lines of code) that would benefit from strengthening.