MutDafny: A Mutation-Based Approach to Assess Dafny Specifications

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.