Program verifiers are widely used to prove the correctness of critical software systems. To build confidence in their results, it is important to develop testing frameworks that help detect bugs in verifiers. Inspired by the success of fuzzing in finding bugs in compilers and SMT solvers, we have built the first fuzzing and differential testing framework for Dafny, a high-level programming language with a Floyd-Hoare-style program verifier and compilers to C#, Java, Go, and Javascript.

This paper presents our experience building and using XDsmith, a testing framework that targets the entire XDsmith toolchain, from verification to compilation. XDsmith randomly generates Dafny programs that are annotated with preconditions, postconditions, and assertions. These programs are used to test the soundness and precision of the Dafny verifier, and to perform differential testing on the four XDsmith compilers. Using XDsmith, we uncovered 31 bugs across the XDsmith verifier and compilers, each of which has been confirmed by the XDsmith developers. Moreover, 8 of these bugs have been fixed in the mainline release of XDsmith.