{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,12]],"date-time":"2026-06-12T04:35:39Z","timestamp":1781238939580,"version":"3.54.1"},"reference-count":45,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2023,4,6]],"date-time":"2023-04-06T00:00:00Z","timestamp":1680739200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2023,4,6]]},"abstract":"<jats:p>The Rust programming language provides a powerful type system that checks linearity and borrowing, allowing code to safely manipulate memory without garbage collection and making Rust ideal for developing low-level, high-assurance systems. For such systems, formal verification can be useful to prove functional correctness properties beyond type safety. This paper presents Verus, an SMT-based tool for formally verifying Rust programs.  \nWith Verus, programmers express proofs and specifications using the Rust language, allowing proofs to take advantage of Rust's linear types and borrow checking. We show how this allows proofs to manipulate linearly typed permissions that let Rust code safely manipulate memory, pointers, and concurrent resources. Verus organizes proofs and specifications using a novel mode system that distinguishes specifications, which are not checked for linearity and borrowing, from executable code and proofs, which are checked for linearity and borrowing.  \nWe formalize Verus' linearity, borrowing, and modes in a small lambda calculus, for which we prove type safety and termination of specifications and proofs. We demonstrate Verus on a series of examples, including pointer-manipulating code (an xor-based doubly linked list), code with interior mutability, and concurrent code.<\/jats:p>","DOI":"10.1145\/3586037","type":"journal-article","created":{"date-parts":[[2023,4,6]],"date-time":"2023-04-06T21:06:02Z","timestamp":1680815162000},"page":"286-315","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":77,"title":["Verus: Verifying Rust Programs using Linear Ghost Types"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9303-452X","authenticated-orcid":false,"given":"Andrea","family":"Lattuada","sequence":"first","affiliation":[{"name":"VMware Research, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-1104-7795","authenticated-orcid":false,"given":"Travis","family":"Hance","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0009-6620-9070","authenticated-orcid":false,"given":"Chanhee","family":"Cho","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-5349-4347","authenticated-orcid":false,"given":"Matthias","family":"Brun","sequence":"additional","affiliation":[{"name":"ETH Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-2401-1682","authenticated-orcid":false,"given":"Isitha","family":"Subasinghe","sequence":"additional","affiliation":[{"name":"UNSW Sydney, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7597-1176","authenticated-orcid":false,"given":"Yi","family":"Zhou","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1781-2473","authenticated-orcid":false,"given":"Jon","family":"Howell","sequence":"additional","affiliation":[{"name":"VMware Research, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9113-1684","authenticated-orcid":false,"given":"Bryan","family":"Parno","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5676-0362","authenticated-orcid":false,"given":"Chris","family":"Hawblitzel","sequence":"additional","affiliation":[{"name":"Microsoft Research, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2023,4,6]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2872362.2872404"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-06773-0_5"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360573"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_17"},{"key":"e_1_2_2_5_1","volume-title":"Proceedings of the 8th International Workshop on Satisfiability Modulo Theories","author":"Barrett Clark","year":"2010","unstructured":"Clark Barrett , Aaron Stump , and Cesare Tinelli . 2010 . The SMT-LIB Standard: Version 2.0 . In Proceedings of the 8th International Workshop on Satisfiability Modulo Theories ( Edinburgh, UK), A. Gupta and D. Kroening (Eds.). Clark Barrett, Aaron Stump, and Cesare Tinelli. 2010. The SMT-LIB Standard: Version 2.0. In Proceedings of the 8th International Workshop on Satisfiability Modulo Theories (Edinburgh, UK), A. Gupta and D. Kroening (Eds.)."},{"key":"e_1_2_2_6_1","unstructured":"Fran\u00e7ois Bobot Jean-Christophe Filli\u00e2tre Claude March\u00e9 and Andrei Paskevich. 2011. Why3: Shepherd Your Herd of Provers. In Boogie 2011: First International Workshop on Intermediate Verification Languages. Wroc\u0142 aw Poland. 53\u201364.  https:\/\/hal.inria.fr\/hal-00790310 \t\t\t\t  Fran\u00e7ois Bobot Jean-Christophe Filli\u00e2tre Claude March\u00e9 and Andrei Paskevich. 2011. Why3: Shepherd Your Herd of Provers. In Boogie 2011: First International Workshop on Intermediate Verification Languages. Wroc\u0142 aw Poland. 53\u201364.  https:\/\/hal.inria.fr\/hal-00790310"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.469460"},{"key":"e_1_2_2_8_1","unstructured":"Coq Development Team. 2022. The Coq Proof Assistant. https:\/\/coq.inria.fr\/ \t\t\t\t  Coq Development Team. 2022. The Coq Proof Assistant. https:\/\/coq.inria.fr\/"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292564"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371102"},{"key":"e_1_2_2_11_1","volume-title":"Proceedings of the Conference on Automated Deduction (CADE).","author":"de Moura Leonardo","year":"2015","unstructured":"Leonardo de Moura , Soonho Kong , Jeremy Avigad , Floris van Doorn , and Jakob von Raumer . 2015 . The Lean Theorem Prover . In Proceedings of the Conference on Automated Deduction (CADE). Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. 2015. The Lean Theorem Prover. In Proceedings of the Conference on Automated Deduction (CADE)."},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73595-3_13"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-17244-1_6"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473590"},{"key":"e_1_2_2_17_1","unstructured":"Google Security Blog. 2021. Rust in the Android platform. https:\/\/security.googleblog.com\/2021\/04\/rust-in-android-platform.html \t\t\t\t  Google Security Blog. 2021. Rust in the Android platform. https:\/\/security.googleblog.com\/2021\/04\/rust-in-android-platform.html"},{"key":"e_1_2_2_18_1","volume-title":"Sharding the State Machine: Automated Modular Reasoning for Complex Concurrent Systems. CyLab","author":"Hance Travis","unstructured":"Travis Hance , Yi Zhou , Andrea Lattuada , Reto Achermann , Alex Conway , Ryan Stutsman , Gerd Zellweger , Chris Hawblitzel , Jon Howell , and Bryan Parno . 2022. Sharding the State Machine: Automated Modular Reasoning for Complex Concurrent Systems. CyLab , Carnegie Mellon University . Travis Hance, Yi Zhou, Andrea Lattuada, Reto Achermann, Alex Conway, Ryan Stutsman, Gerd Zellweger, Chris Hawblitzel, Jon Howell, and Bryan Parno. 2022. Sharding the State Machine: Automated Modular Reasoning for Complex Concurrent Systems. CyLab, Carnegie Mellon University."},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547647"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_4"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371109"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158154"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_2_2_24_1","volume-title":"The Rust Programming Language","author":"Klabnik Steve","unstructured":"Steve Klabnik and Carol Nichols . 2018. The Rust Programming Language . No Starch Press, USA. isbn:1593278284 Steve Klabnik and Carol Nichols. 2018. The Rust Programming Language. No Starch Press, USA. isbn:1593278284"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.7511039"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.7718486"},{"key":"e_1_2_2_27_1","volume-title":"Verus: Verifying Rust Programs using Linear Ghost Types (extended version). https:\/\/doi.org\/10.48550\/ARXIV.2303.05491","author":"Lattuada Andrea","year":"2023","unstructured":"Andrea Lattuada , Travis Hance , Chanhee Cho , Matthias Brun , Isitha Subasinghe , Yi Zhou , Jon Howell , Bryan Parno , and Chris Hawblitzel . 2023 . Verus: Verifying Rust Programs using Linear Ghost Types (extended version). https:\/\/doi.org\/10.48550\/ARXIV.2303.05491 10.48550\/ARXIV.2303.05491 Andrea Lattuada, Travis Hance, Chanhee Cho, Matthias Brun, Isitha Subasinghe, Yi Zhou, Jon Howell, Bryan Parno, and Chris Hawblitzel. 2023. Verus: Verifying Rust Programs using Linear Ghost Types (extended version). https:\/\/doi.org\/10.48550\/ARXIV.2303.05491"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_2_2_29_1","volume-title":"Conference: Tools and Algorithms for the Construction and Analysis of Systems, 16th International Conference, TACAS","author":"Leino Rustan","year":"2010","unstructured":"Rustan Leino and Philipp R\u00fcmmer . 2010. A Polymorphic Intermediate Verification Language: Design and Logical Encoding . In Conference: Tools and Algorithms for the Construction and Analysis of Systems, 16th International Conference, TACAS 2010 , Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus , March 20-28, 2010.. https:\/\/doi.org\/978-3-642-12002-2_26 Rustan Leino and Philipp R\u00fcmmer. 2010. A Polymorphic Intermediate Verification Language: Design and Logical Encoding. In Conference: Tools and Algorithms for the Construction and Analysis of Systems, 16th International Conference, TACAS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010.. https:\/\/doi.org\/978-3-642-12002-2_26"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3527313"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2692956.2663188"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523704"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-44914-8_18"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/11417170_22"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_2"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.035"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3443420"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_2_2_39_1","volume-title":"Alias Types. In Proceedings of the 9th European Symposium on Programming Languages and Systems (ESOP \u201900)","author":"Smith Frederick","unstructured":"Frederick Smith , David Walker , and J. Gregory Morrisett . 2000 . Alias Types. In Proceedings of the 9th European Symposium on Programming Languages and Systems (ESOP \u201900) . Frederick Smith, David Walker, and J. Gregory Morrisett. 2000. Alias Types. In Proceedings of the 9th European Symposium on Programming Languages and Systems (ESOP \u201900)."},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"},{"key":"e_1_2_2_41_1","volume-title":"Linus Torvalds: Rust will go into Linux 6.1. https:\/\/www.zdnet.com\/article\/linus-torvalds-rust-will-go-into-linux-6-1\/","author":"Vaughan-Nichols Steven","year":"2022","unstructured":"Steven Vaughan-Nichols . 2022 . Linus Torvalds: Rust will go into Linux 6.1. https:\/\/www.zdnet.com\/article\/linus-torvalds-rust-will-go-into-linux-6-1\/ Steven Vaughan-Nichols. 2022. Linus Torvalds: Rust will go into Linux 6.1. https:\/\/www.zdnet.com\/article\/linus-torvalds-rust-will-go-into-linux-6-1\/"},{"issue":"2","key":"e_1_2_2_42_1","first-page":"2","article-title":"Linear Types can Change the World!. In Programming concepts and methods","volume":"2","author":"Wadler Philip","year":"1990","unstructured":"Philip Wadler . 1990 . Linear Types can Change the World!. In Programming concepts and methods : Proceedings of the IFIP Working Group 2 . 2 , 2 .3 Working Conference on Programming Concepts and Methods, Sea of Galilee, Israel, 2-5 April, 1990. North-Holland, 561. Philip Wadler. 1990. Linear Types can Change the World!. In Programming concepts and methods: Proceedings of the IFIP Working Group 2.2, 2.3 Working Conference on Programming Concepts and Methods, Sea of Galilee, Israel, 2-5 April, 1990. North-Holland, 561.","journal-title":"Proceedings of the IFIP Working Group"},{"key":"e_1_2_2_43_1","volume-title":"Oxide: The Essence of Rust. CoRR, abs\/1903.00982","author":"Weiss Aaron","year":"2019","unstructured":"Aaron Weiss , Daniel Patterson , Nicholas D. Matsakis , and Amal Ahmed . 2019 . Oxide: The Essence of Rust. CoRR, abs\/1903.00982 (2019), arXiv:1903.00982. arxiv:1903.00982 Aaron Weiss, Daniel Patterson, Nicholas D. Matsakis, and Amal Ahmed. 2019. Oxide: The Essence of Rust. CoRR, abs\/1903.00982 (2019), arXiv:1903.00982. arxiv:1903.00982"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473597"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30557-6_8"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3586037","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3586037","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:46:10Z","timestamp":1750178770000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3586037"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,4,6]]},"references-count":45,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2023,4,6]]}},"alternative-id":["10.1145\/3586037"],"URL":"https:\/\/doi.org\/10.1145\/3586037","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,4,6]]},"assertion":[{"value":"2023-04-06","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}