Helping Users to Reduce Brittleness in Dafny Programs - A Success Story

This conference talk explores how to reduce brittleness in Dafny programs, presented by Remy Willems, Matthias Schlaipfer, and Olivier Bouissou from Amazon at the Dafny 2025 workshop. Learn about the critical problem of proof instability in SMT-based automated program verifiers, where small changes to programs or tool versions can cause SMT solvers to take much longer or fail completely. Discover manual language features that go beyond previously proposed automated methods for reducing brittleness. The presenters demonstrate through various examples and code deployed at scale at a major cloud provider that these techniques are developer-friendly and significantly impactful. The talk was sponsored by ACM SIGPLAN and presented at the Dafny 2025 workshop on January 19, 2025.