Verified VCG and Verified Compiler for Dafny
Daniel Nezamabadi, Magnus O. Myreen, Yong Kiam Tan
TL;DR
<3-5 sentence high-level summary> The paper tackles trust gaps in Dafny's verifier and compiler by building a foundational, end-to-end verification pipeline. It defines a functional big-step semantics for a substantial imperative subset of Dafny (including mutual recursion, while loops, and arrays) and then derives a verified verification condition generator (VCG) and a verified compiler to CakeML, all mechanized in HOL4. The compiler translates Dafny to CakeML and, via CakeML's own verified backend, to machine code, preserving proven functional correctness. The work demonstrates that a fully verified Dafny toolchain is feasible and provides a blueprint for trustworthy verification-aware programming ecosystems.
Abstract
Dafny is a verification-aware programming language that comes with a compiler and static program verifier. However, neither the compiler nor the verifier is proved correct; in fact, soundness bugs have been found in both tools. This paper shows that the aforementioned Dafny tools can be developed with foundational correctness guarantees. We present a functional big-step semantics for an imperative subset of Dafny and, based on this semantics, a verified verification condition generator (VCG) and a verified compiler for Dafny. The subset of Dafny we have formalized includes mutually recursive method calls, while loops, and arrays -- these language features are significant enough to cover challenging examples such as McCarthy's 91 function and array-based programs that are used when teaching Dafny. The verified VCG allows one to prove functional correctness of annotated Dafny programs, while the verified compiler can be used to compile verified Dafny programs to CakeML programs. From there, one can obtain executable machine code via the (already verified) CakeML compiler, all while provably maintaining the functional correctness guarantees that were proved for the source-level Dafny programs. Our work has been mechanized in the HOL4 theorem prover.