Explore how auto-active verifiers like Dafny impact real-world software development through this 15-minute conference presentation from OOPSLA 2025. Learn about findings from interviews with 14 experienced Dafny users who applied formal verification in large-scale projects, examining the practical challenges and barriers to adoption despite SMT automation and programmer-friendly features. Discover insights from grounded theory analysis that systematically identifies how auto-active verification affects software development workflows and uncover opportunities to simplify verification tools to expand their adoption in industry. Gain understanding of the significant effort required to apply formal methods in practice and the research-backed recommendations for making verification more accessible to non-expert developers. Access supplementary materials including the full research article and artifact archive to deepen your knowledge of formal verification's role in modern software engineering.