{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T18:11:50Z","timestamp":1760033510001,"version":"build-2065373602"},"reference-count":64,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,10,9]]},"abstract":"<jats:p>Auto-active verifiers like Dafny aim to make formal methods accessible to non-expert users through SMT automation. However, despite the automation and other programmer-friendly features, they remain sparsely used in real-world software development, due to the significant effort required to apply them in practice. We interviewed 14 experienced Dafny users about their experiences using it in large-scale projects. We apply grounded theory to analyze the interviews to systematically identify how auto-active verification impacts software development, and to identify opportunities to simplify the use, and hence, expand the adoption of verification in software development.<\/jats:p>","DOI":"10.1145\/3763181","type":"journal-article","created":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T08:49:50Z","timestamp":1759999790000},"page":"3642-3668","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["On the Impact of Formal Verification on Software Development"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0009-0006-4967-6820","authenticated-orcid":false,"given":"Eric","family":"Mugnier","sequence":"first","affiliation":[{"name":"University of California at San Diego, La Jolla, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-0980-2538","authenticated-orcid":false,"given":"Yuanyuan","family":"Zhou","sequence":"additional","affiliation":[{"name":"University of California at San Diego, La Jolla, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1802-9421","authenticated-orcid":false,"given":"Ranjit","family":"Jhala","sequence":"additional","affiliation":[{"name":"University of California at San Diego, La Jolla, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9369-4069","authenticated-orcid":false,"given":"Michael","family":"Coblenz","sequence":"additional","affiliation":[{"name":"University of California at San Diego, La Jolla, USA"}]}],"member":"320","published-online":{"date-parts":[[2025,10,9]]},"reference":[{"volume-title":"https:\/\/github.com\/microsoft\/Ironclad\/blob\/2fe4dcdc323b92e93f759cc3e373521366b7f691\/ironfleet\/src\/Dafny\/Distributed\/Impl\/Common\/UpperBound.i.dfy#L10","unstructured":"2015. UpperBound.i.dfy. https:\/\/github.com\/microsoft\/Ironclad\/blob\/2fe4dcdc323b92e93f759cc3e373521366b7f691\/ironfleet\/src\/Dafny\/Distributed\/Impl\/Common\/UpperBound.i.dfy#L10","key":"e_1_2_1_1_1"},{"unstructured":"2023. Dafny VMC Guidelines. https:\/\/github.com\/dafny-lang\/Dafny-VMC\/blob\/main\/Guidelines.md","key":"e_1_2_1_2_1"},{"unstructured":"2023. Verification Optimization. https:\/\/dafny.org\/latest\/VerificationOptimization\/VerificationOptimization","key":"e_1_2_1_3_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_4_1","DOI":"10.1016\/j.jss.2012.01.059"},{"doi-asserted-by":"publisher","key":"e_1_2_1_5_1","DOI":"10.1006\/jsco.1997.0175"},{"doi-asserted-by":"publisher","key":"e_1_2_1_6_1","DOI":"10.1109\/ICSE.2012.6227120"},{"unstructured":"RS Arnold and SA Bohner. 1996. An introduction to software change impact analysis. Software Change Impact Analysis 1\u201326.","key":"e_1_2_1_7_1"},{"key":"e_1_2_1_8_1","volume-title":"Duvet: A requirements traceability tool. https:\/\/github.com\/awslabs\/duvet","author":"Labs AWS","year":"2025","unstructured":"AWS Labs. 2025. Duvet: A requirements traceability tool. https:\/\/github.com\/awslabs\/duvet"},{"doi-asserted-by":"publisher","key":"e_1_2_1_9_1","DOI":"10.1145\/3586030"},{"doi-asserted-by":"publisher","unstructured":"Scott O. Bradner. 1997. Key words for use in RFCs to Indicate Requirement Levels. RFC 2119. https:\/\/doi.org\/10.17487\/RFC2119 10.17487\/RFC2119","key":"e_1_2_1_10_1","DOI":"10.17487\/RFC2119"},{"doi-asserted-by":"publisher","key":"e_1_2_1_11_1","DOI":"10.1007\/978-3-030-99524-9_23"},{"doi-asserted-by":"crossref","unstructured":"Aleks Chakarov Jaco Geldenhuys Matthew Heck Mike Hicks Sam Huang Georges Axel Jaloyan Anjali Joshi Rustan Leino Mikael Mayer Sean McLaughlin Akhilesh Mritunjai Cl\u00e9ment Pit Claudel Sorawee Porncharoenwase Florian Rabe Marianna Rapoport Giles Reger Cody Roux Neha Rungta Robin Salkeld Matthias Schlaipfer Daniel Schoepe Johanna Schwartzentruber Serdar Tasiran Aaron Tomb Emina Torlak John Tristan Lucas Wagner Mike Whalen Remy Willems Jenny Xiang Tae Joon Byun Joshua Cohen Ruijie Wang Junyoung Jang Jakob Rath Hira Taqdees Syeda Dominik Wagner and Yongwei Yuan. 2025. Formally verified cloud-scale authorization. https:\/\/www.amazon.science\/publications\/formally-verified-cloud-scale-authorization","key":"e_1_2_1_12_1","DOI":"10.1109\/ICSE55347.2025.00166"},{"unstructured":"Kathy Charmaz. 2014. Constructing grounded theory. SAGE publications Ltd.","key":"e_1_2_1_13_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_14_1","DOI":"10.1007\/978-3-031-65627-9_17"},{"doi-asserted-by":"publisher","key":"e_1_2_1_15_1","DOI":"10.1145\/3452379"},{"unstructured":"J. de Muijnck-Hughes and J. Noble. 2024. Colouring Flags with Dafny & Idris.","key":"e_1_2_1_16_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_17_1","DOI":"10.1016\/J.SCICO.2007.01.015"},{"unstructured":"Jo\u00e3o Pascoal Faria and Rui Abreu. 2023. Case Studies of\u00a0Development of\u00a0Verified Programs with\u00a0Dafny for\u00a0Accessibility Assessment. In Fundamentals of Software Engineering. isbn:978-3-031-42441-0","key":"e_1_2_1_18_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_19_1","DOI":"10.1145\/263244.263267"},{"key":"e_1_2_1_20_1","volume-title":"Seventeenth Symposium on Usable Privacy and Security (SOUPS 2021","author":"Fulton Kelsey R.","year":"2021","unstructured":"Kelsey R. Fulton, Anna Chan, Daniel Votipka, Michael Hicks, and Michelle L. Mazurek. 2021. Benefits and Drawbacks of Adopting a Secure Programming Language: Rust as a Case Study. In Seventeenth Symposium on Usable Privacy and Security (SOUPS 2021). USENIX Association, 597\u2013616. isbn:978-1-939133-25-0 https:\/\/www.usenix.org\/conference\/soups2021\/presentation\/fulton"},{"doi-asserted-by":"publisher","key":"e_1_2_1_21_1","DOI":"10.1145\/3729327"},{"key":"e_1_2_1_22_1","volume-title":"IronSpec: Increasing the Reliability of Formal Specifications. In 18th USENIX Symposium on Operating Systems Design and Implementation (OSDI 24)","author":"Goldweber Eli","year":"2024","unstructured":"Eli Goldweber, Weixin Yu, Seyed Armin Vakil Ghahani, and Manos Kapritsos. 2024. IronSpec: Increasing the Reliability of Formal Specifications. In 18th USENIX Symposium on Operating Systems Design and Implementation (OSDI 24). USENIX Association, Santa Clara, CA. 875\u2013891. isbn:978-1-939133-40-3 https:\/\/www.usenix.org\/conference\/osdi24\/presentation\/goldweber"},{"doi-asserted-by":"publisher","key":"e_1_2_1_23_1","DOI":"10.1177\/1525822X05279903"},{"doi-asserted-by":"publisher","key":"e_1_2_1_24_1","DOI":"10.1145\/2815400.2815428"},{"unstructured":"Li Huang Sophie Ebersold Alexander Kogtenkov Bertrand Meyer and Yinling Liu. 2024. Lessons from Formally Verified Deployed Software Systems (Extended version). arxiv:2301.02206. arxiv:2301.02206","key":"e_1_2_1_25_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_26_1","DOI":"10.1007\/978-3-031-42753-4_10"},{"doi-asserted-by":"publisher","key":"e_1_2_1_27_1","DOI":"10.1145\/3533767.3534382"},{"doi-asserted-by":"publisher","key":"e_1_2_1_28_1","DOI":"10.1145\/1629575.1629596"},{"doi-asserted-by":"publisher","key":"e_1_2_1_29_1","DOI":"10.1145\/3586037"},{"doi-asserted-by":"publisher","key":"e_1_2_1_30_1","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_2_1_31_1","volume-title":"Usable Verification Workshop.","author":"Leino K Rustan M","year":"2010","unstructured":"K Rustan M Leino and Micha\u0142 Moskal. 2010. Usable auto-active verification. In Usable Verification Workshop."},{"key":"e_1_2_1_32_1","volume-title":"Marktoberdorf International Summer School","author":"Leino Rustan","year":"2008","unstructured":"Rustan Leino. 2008. Specification and Verification of Object-Oriented Software. In Marktoberdorf International Summer School 2008. https:\/\/www.microsoft.com\/en-us\/research\/publication\/specification-verification-object-oriented-software\/"},{"doi-asserted-by":"publisher","key":"e_1_2_1_33_1","DOI":"10.1145\/1111037.1111042"},{"doi-asserted-by":"publisher","key":"e_1_2_1_34_1","DOI":"10.1145\/3485532"},{"unstructured":"Simon Marlow. 2010. Haskell 2010 Language Report. 07.","key":"e_1_2_1_35_1"},{"key":"e_1_2_1_36_1","volume-title":"Clean Code: A Handbook of Agile Software Craftsmanship (1 ed.)","author":"Martin Robert C.","year":"2008","unstructured":"Robert C. Martin. 2008. Clean Code: A Handbook of Agile Software Craftsmanship (1 ed.). Prentice Hall PTR, USA. isbn:0132350882"},{"doi-asserted-by":"publisher","key":"e_1_2_1_37_1","DOI":"10.1145\/3359174"},{"doi-asserted-by":"publisher","key":"e_1_2_1_38_1","DOI":"10.48550\/ARXIV.2207.10424"},{"doi-asserted-by":"publisher","key":"e_1_2_1_39_1","DOI":"10.1145\/3720499"},{"doi-asserted-by":"publisher","unstructured":"Eric Mugnier Yuanyuan Zhou Ranjit Jhala and Michael Coblenz. 2025. Artifact for \"On the Impact of Formal Verification on Software Development\". https:\/\/doi.org\/10.5281\/zenodo.15761040 10.5281\/zenodo.15761040","key":"e_1_2_1_40_1","DOI":"10.5281\/zenodo.15761040"},{"key":"e_1_2_1_41_1","volume-title":"Paulson","author":"Nipkow Tobias","year":"2002","unstructured":"Tobias Nipkow, Markus Wenzel, and Lawrence C. Paulson. 2002. Isabelle\/HOL: a proof assistant for higher-order logic. Springer-Verlag, Berlin, Heidelberg. isbn:3540433767"},{"unstructured":"James Noble. 2024. Learn \u2019em Dafny!.","key":"e_1_2_1_42_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_43_1","DOI":"10.1145\/3678721.3686228"},{"key":"e_1_2_1_44_1","volume-title":"A Philosophy of Software Design","author":"Ousterhout John","unstructured":"John Ousterhout. 2018. A Philosophy of Software Design (1st ed.). isbn:1732102201","edition":"1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_45_1","DOI":"10.1145\/2846680.2846691"},{"key":"e_1_2_1_46_1","volume-title":"Pearce and Lindsay Groves","author":"David","year":"2013","unstructured":"David J. Pearce and Lindsay Groves. 2013. Whiley: A Platform for Research in Software Verification. In Software Language Engineering. Springer International Publishing, Cham. 238\u2013248. isbn:978-3-319-02654-1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_47_1","DOI":"10.1145\/3236024.3236080"},{"doi-asserted-by":"publisher","key":"e_1_2_1_48_1","DOI":"10.1145\/3622851"},{"unstructured":"Microsoft Research. 2015. Ironfleet Style Guide. https:\/\/github.com\/microsoft\/Ironclad\/blob\/2fe4dcdc323b92e93f759cc3e373521366b7f691\/ironfleet\/STYLE.md","key":"e_1_2_1_49_1"},{"unstructured":"Talia Ringer. 2020. Mechanized Proofs for PL: Past Present and Future. https:\/\/blog.sigplan.org\/2020\/01\/29\/mechanized-proofs-for-pl-past-present-and-future\/","key":"e_1_2_1_50_1"},{"doi-asserted-by":"publisher","unstructured":"Talia Ringer Karl Palmskog Ilya Sergey Milos Gligoric and Zachary Tatlock. 2019. QED at Large: A Survey of Engineering of Formally Verified Software. Found. Trends Program. Lang. https:\/\/doi.org\/10.1561\/2500000045 10.1561\/2500000045","key":"e_1_2_1_51_1","DOI":"10.1561\/2500000045"},{"doi-asserted-by":"crossref","unstructured":"Neha Rungta. 2024. Trillions of Formally Verified Authorizations a day!. https:\/\/2024.splashcon.org\/details\/splash-2024-keynotes\/3\/Trillions-of-Formally-Verified-Authorizations-a-day-","key":"e_1_2_1_52_1","DOI":"10.1145\/3689491.3700409"},{"doi-asserted-by":"publisher","key":"e_1_2_1_53_1","DOI":"10.1007\/978-3-662-46669-8_33"},{"doi-asserted-by":"publisher","unstructured":"Jessica Shi Cassia Torczon Harrison Goldstein Benjamin C. Pierce and Andrew Head. 2025. QED in Context: An Observation Study of Proof Assistant Users. OOPSLA https:\/\/doi.org\/10.1145\/3720426 10.1145\/3720426","key":"e_1_2_1_54_1","DOI":"10.1145\/3720426"},{"doi-asserted-by":"publisher","key":"e_1_2_1_55_1","DOI":"10.1145\/2652524.2652551"},{"key":"e_1_2_1_56_1","volume-title":"Anvil: Verifying Liveness of Cluster Management Controllers. In 18th USENIX Symposium on Operating Systems Design and Implementation (OSDI 24)","author":"Sun Xudong","year":"2024","unstructured":"Xudong Sun, Wenjie Ma, Jiawei Tyler Gu, Zicheng Ma, Tej Chajed, Jon Howell, Andrea Lattuada, Oded Padon, Lalith Suresh, Adriana Szekeres, and Tianyin Xu. 2024. Anvil: Verifying Liveness of Cluster Management Controllers. In 18th USENIX Symposium on Operating Systems Design and Implementation (OSDI 24). USENIX Association, Santa Clara, CA. 649\u2013666. isbn:978-1-939133-40-3 https:\/\/www.usenix.org\/conference\/osdi24\/presentation\/sun-xudong"},{"doi-asserted-by":"publisher","unstructured":"Nikhil Swamy C\u0103t\u0103lin Hri\u0163cu Chantal Keller Aseem Rastogi Antoine Delignat-Lavaud Simon Forest Karthikeyan Bhargavan C\u00e9dric Fournet Pierre-Yves Strub Markulf Kohlweiss Jean-Karim Zinzindohoue and Santiago Zanella-B\u00e9guelin. 2016. Dependent Types and Multi-Monadic Effects in F*. In Principles of Programming Languages (POPL). https:\/\/doi.org\/10.1145\/2837614.2837655 10.1145\/2837614.2837655","key":"e_1_2_1_57_1","DOI":"10.1145\/2837614.2837655"},{"doi-asserted-by":"publisher","key":"e_1_2_1_58_1","DOI":"10.1145\/3519939.3523708"},{"unstructured":"Aaron Tomb. 2023. Clear Separation of Specification and Implementation in Dafny. https:\/\/dafny.org\/blog\/2023\/08\/14\/clear-specification-and-implementation\/","key":"e_1_2_1_59_1"},{"key":"e_1_2_1_60_1","volume-title":"LiquidHaskell. In Proceedings of the 2014 ACM SIGPLAN symposium on Haskell.","author":"Vazou Niki","year":"2014","unstructured":"Niki Vazou, Eric L Seidel, and Ranjit Jhala. 2014. LiquidHaskell. In Proceedings of the 2014 ACM SIGPLAN symposium on Haskell."},{"doi-asserted-by":"publisher","key":"e_1_2_1_61_1","DOI":"10.1109\/ICSE.2015.54"},{"doi-asserted-by":"publisher","key":"e_1_2_1_62_1","DOI":"10.1145\/362575.362577"},{"doi-asserted-by":"publisher","unstructured":"Yi Zhou Jay Bosamiya Yoshiki Takashima Jessica Li Marijn Heule and Bryan Parno. 2023. Mariposa: Measuring SMT Instability in Automated Program Verification. In 2023 Formal Methods in Computer-Aided Design (FMCAD). 178\u2013188. https:\/\/doi.org\/10.34727\/2023\/isbn.978-3-85448-060-0_26 10.34727\/2023\/isbn.978-3-85448-060-0_26","key":"e_1_2_1_63_1","DOI":"10.34727\/2023\/isbn.978-3-85448-060-0_26"},{"key":"e_1_2_1_64_1","volume-title":"VeriSMo: A Verified Security Module for Confidential VMs. In 18th USENIX Symposium on Operating Systems Design and Implementation (OSDI 24)","author":"Zhou Ziqiao","year":"2024","unstructured":"Ziqiao Zhou, Anjali, Weiteng Chen, Sishuai Gong, Chris Hawblitzel, and Weidong Cui. 2024. VeriSMo: A Verified Security Module for Confidential VMs. In 18th USENIX Symposium on Operating Systems Design and Implementation (OSDI 24). USENIX Association, Santa Clara, CA. 599\u2013614. isbn:978-1-939133-40-3 https:\/\/www.usenix.org\/conference\/osdi24\/presentation\/zhou"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3763181","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T17:46:43Z","timestamp":1760032003000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3763181"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,9]]},"references-count":64,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2025,10,9]]}},"alternative-id":["10.1145\/3763181"],"URL":"https:\/\/doi.org\/10.1145\/3763181","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2025,10,9]]},"assertion":[{"value":"2025-03-26","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-08-12","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-10-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}