Proof, but at What Cost?

No ratings

Presented at High Confidence Software and Systems Conference 2022 by

Robin Salkeld

Dafny is a verification-aware programming language that aims to make formal verification more accessible to programmers and students. The Dafny toolchain includes a verifier that translates Dafny programs to Boogie, an intermediate verification language that supports verifying specifications by invoking an SMT solver such as Z3. While Dafny has been heavily used for research and education for years, it is now starting to be used for production industrial projects, and multiple recent projects within Amazon Web Services (AWS) with high assurance requirements have been written in Dafny. Through this increase in usage, especially by software engineers that are not necessarily well-versed in formal verification, the Dafny core team at AWS has observed that the biggest threat to Dafny adoption by far is “verification instability.” This is the phenomenon where small, seemingly unrelated changes to Dafny code cause previously-verified specifications to no longer verify. This is a known consequence of the “butterfly effect” of SMT solvers in the field, but greatly impacts engineers’ willingness to adopt Dafny. Verification instability can turn a small bug fix task into a week-long ordeal to fix verification of code the engineer has no familiarity with, and makes predictable software development extremely difficult. It also impacts engineers’ trust in the Dafny platform, as they begin to doubt whether the broken verification was actually sound in the first place. In this talk, we will describe recent advances in preventing and mitigating verification instability on the Dafny platform. Our key insight based on empirical data from multiple Dafny projects is that the cost of verification correlates strongly with future verification instability. We describe new features in Dafny and Boogie to provide more stable verification, and to support a continuous integration mechanism that rejects Dafny code that successfully verifies but takes longer than a configured timeout, and hence is likely to exhibit future instability. We show how these improvements helped to provide a more efficient and predictable development velocity for at least one new Dafny project. We conclude with a call to action for SMT solvers to provide the deterministic behavior and metrics needed to support this workflow.