{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T06:22:17Z","timestamp":1784182937371,"version":"3.55.0"},"reference-count":48,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2022,8,29]],"date-time":"2022-08-29T00:00:00Z","timestamp":1661731200000},"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":[[2022,8,29]]},"abstract":"<jats:p>We present Aeneas, a new verification toolchain for Rust programs based on a lightweight functional translation. We leverage Rust\u2019s rich region-based type system to eliminate memory reasoning for a large class of Rust programs, as long as they do not rely on interior mutability or unsafe code. Doing so, we relieve the proof engineer of the burden of memory-based reasoning, allowing them to instead focus on functional properties of their code.<\/jats:p>\n          <jats:p>The first contribution of Aeneas is a new approach to borrows and controlled aliasing. We propose a pure, functional semantics for LLBC, a Low-Level Borrow Calculus that captures a large subset of Rust programs. Our semantics is value-based, meaning there is no notion of memory, addresses or pointer arithmetic. Our semantics is also ownership-centric, meaning that we enforce soundness of borrows via a semantic criterion based on loans rather than through a syntactic type-based lifetime discipline. We claim that our semantics captures the essence of the borrow mechanism rather than its current implementation in the Rust compiler.<\/jats:p>\n          <jats:p>The second contribution of Aeneas is a translation from LLBC to a pure lambda-calculus. This allows the user to reason about the original Rust program through the theorem prover of their choice, and fulfills our promise of enabling lightweight verification of Rust programs. To deal with the well-known technical difficulty of terminating a borrow, we rely on a novel approach, in which we approximate the borrow graph in the presence of function calls. This in turn allows us to perform the translation using a new technical device called backward functions.<\/jats:p>\n          <jats:p>We implement our toolchain in a mixture of Rust and OCaml; our chief case study is a low-level, resizing hash table, for which we prove functional correctness, the first such result in Rust. Our evaluation shows significant gains of verification productivity for the programmer. This paper therefore establishes a new point in the design space of Rust verification toolchains, one that aims to verify Rust programs simply, and at scale.<\/jats:p>\n          <jats:p>Rust goes to great lengths to enforce static control of aliasing; the proof engineer should not waste any time on memory reasoning when so much already comes \u201cfor free\u201d!<\/jats:p>","DOI":"10.1145\/3547647","type":"journal-article","created":{"date-parts":[[2022,8,31]],"date-time":"2022-08-31T19:39:26Z","timestamp":1661974766000},"page":"711-741","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":48,"title":["Aeneas: Rust verification by functional translation"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3297-9156","authenticated-orcid":false,"given":"Son","family":"Ho","sequence":"first","affiliation":[{"name":"Inria, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7347-3050","authenticated-orcid":false,"given":"Jonathan","family":"Protzenko","sequence":"additional","affiliation":[{"name":"Microsoft Research, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,8,31]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"2017. Not possible to bind to a pattern. https:\/\/github.com\/FStarLang\/FStar\/issues\/1288 \t\t\t\t  2017. Not possible to bind to a pattern. https:\/\/github.com\/FStarLang\/FStar\/issues\/1288"},{"key":"e_1_2_1_2_1","unstructured":"2021. StackOverflow Developer Survey. https:\/\/insights.stackoverflow.com\/survey\/2021 \t\t\t\t  2021. StackOverflow Developer Survey. https:\/\/insights.stackoverflow.com\/survey\/2021"},{"key":"e_1_2_1_3_1","unstructured":"2022. Verus an Experimental Verification Framework for Rust-like code. https:\/\/github.com\/secure-foundations\/verus\/blob\/004eadd8c31b60c886f7a8c8b568806e46a49a78\/source\/docs\/design\/returning-mutable-references.md \t\t\t\t  2022. Verus an Experimental Verification Framework for Rust-like code. https:\/\/github.com\/secure-foundations\/verus\/blob\/004eadd8c31b60c886f7a8c8b568806e46a49a78\/source\/docs\/design\/returning-mutable-references.md"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2980024.2872404"},{"key":"e_1_2_1_5_1","unstructured":"Qinxiang Cao Andrew W Appel Lennart Beringer. 2021. Verifiable C. https:\/\/softwarefoundations.cis.upenn.edu\/vc-current\/index.html \t\t\t\t  Qinxiang Cao Andrew W Appel Lennart Beringer. 2021. Verifiable C. https:\/\/softwarefoundations.cis.upenn.edu\/vc-current\/index.html"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360573"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837022"},{"key":"e_1_2_1_8_1","volume-title":"An Introduction to B\u220a -trees and Write-Optimization. login Usenix Mag., 40","author":"Bender Michael A.","year":"2015","unstructured":"Michael A. Bender , Martin Farach-Colton , William Jannen , Rob Johnson , Bradley C. Kuszmaul , Donald E. Porter , Jun Yuan , and Yang Zhan . 2015. An Introduction to B\u220a -trees and Write-Optimization. login Usenix Mag., 40 ( 2015 ). Michael A. Bender, Martin Farach-Colton, William Jannen, Rob Johnson, Bradley C. Kuszmaul, Donald E. Porter, Jun Yuan, and Yang Zhan. 2015. An Introduction to B\u220a -trees and Write-Optimization. login Usenix Mag., 40 (2015)."},{"key":"e_1_2_1_9_1","volume-title":"Everest: Towards a verified, drop-in replacement of HTTPS. In 2nd Summit on Advances in Programming Languages (SNAPL","author":"Bhargavan Karthikeyan","year":"2017","unstructured":"Karthikeyan Bhargavan , Barry Bond , Antoine Delignat-Lavaud , C\u00e9dric Fournet , Chris Hawblitzel , Catalin Hritcu , Samin Ishtiaq , Markulf Kohlweiss , Rustan Leino , and Jay Lorch . 2017 . Everest: Towards a verified, drop-in replacement of HTTPS. In 2nd Summit on Advances in Programming Languages (SNAPL 2017). Karthikeyan Bhargavan, Barry Bond, Antoine Delignat-Lavaud, C\u00e9dric Fournet, Chris Hawblitzel, Catalin Hritcu, Samin Ishtiaq, Markulf Kohlweiss, Rustan Leino, and Jay Lorch. 2017. Everest: Towards a verified, drop-in replacement of HTTPS. In 2nd Summit on Advances in Programming Languages (SNAPL 2017)."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328487"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45337-7_2"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-9457-5"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411235"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/286936.286947"},{"key":"e_1_2_1_15_1","unstructured":"Xavier Denis Jacques-Henri Jourdan and Claude March\u00e9. 2021. The Creusot Environment for the Deductive Verification of Rust Programs. Inria Saclay - \u00cele de France. https:\/\/hal.inria.fr\/hal-03526634 \t\t\t\t  Xavier Denis Jacques-Henri Jourdan and Claude March\u00e9. 2021. The Creusot Environment for the Deductive Verification of Rust Programs. Inria Saclay - \u00cele de France. https:\/\/hal.inria.fr\/hal-03526634"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132782"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/11693024_2"},{"key":"e_1_2_1_18_1","volume-title":"11th USENIX Symposium on Operating Systems Design and Implementation (OSDI 14)","author":"Hawblitzel Chris","year":"2014","unstructured":"Chris Hawblitzel , Jon Howell , Jacob R Lorch , Arjun Narayan , Bryan Parno , Danfeng Zhang , and Brian Zill . 2014 . Ironclad Apps:$End-to-End$ Security via Automated $Full-System$ Verification . In 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI 14) . 165\u2013181. Chris Hawblitzel, Jon Howell, Jacob R Lorch, Arjun Narayan, Bryan Parno, Danfeng Zhang, and Brian Zill. 2014. Ironclad Apps:$End-to-End$ Security via Automated $Full-System$ Verification. In 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI 14). 165\u2013181."},{"key":"e_1_2_1_19_1","volume-title":"Aeneas: A Verification Toolchain for Rust Programs. https:\/\/github.com\/sonmarcho\/aeneas","author":"Ho Son","year":"2022","unstructured":"Son Ho and Jonathan Protzenko . 2022 . Aeneas: A Verification Toolchain for Rust Programs. https:\/\/github.com\/sonmarcho\/aeneas Son Ho and Jonathan Protzenko. 2022. Aeneas: A Verification Toolchain for Rust Programs. https:\/\/github.com\/sonmarcho\/aeneas"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.6672939"},{"key":"e_1_2_1_21_1","volume-title":"Aeneas: Rust Verification by Functional Translation (Long Version). https:\/\/doi.org\/10.48550\/ARXIV.2206.07185","author":"Ho Son","year":"2022","unstructured":"Son Ho and Jonathan Protzenko . 2022 . Aeneas: Rust Verification by Functional Translation (Long Version). https:\/\/doi.org\/10.48550\/ARXIV.2206.07185 Son Ho and Jonathan Protzenko. 2022. Aeneas: Rust Verification by Functional Translation (Long Version). https:\/\/doi.org\/10.48550\/ARXIV.2206.07185"},{"key":"e_1_2_1_22_1","doi-asserted-by":"crossref","unstructured":"Son Ho Jonathan Protzenko Abhishek Bichhawat and Karthikeyan Bhargavan. 2021. Noise*: A Library of Verified High-Performance Secure Channel Protocol Implementations. \t\t\t\t  Son Ho Jonathan Protzenko Abhishek Bichhawat and Karthikeyan Bhargavan. 2021. Noise*: A Library of Verified High-Performance Secure Channel Protocol Implementations.","DOI":"10.1109\/SP46214.2022.9833621"},{"key":"e_1_2_1_23_1","unstructured":"Graydon Hoare. 2022. https:\/\/twitter.com\/graydon_pub\/status\/1492792051657629698 \t\t\t\t  Graydon Hoare. 2022. https:\/\/twitter.com\/graydon_pub\/status\/1492792051657629698"},{"key":"e_1_2_1_24_1","volume-title":"Viper: A verification infrastructure for permission-based reasoning. ETH Zurich.","author":"Juhasz Uri","year":"2014","unstructured":"Uri Juhasz , Ioannis T Kassios , Peter M\u00fcller , Milos Novacek , Malte Schwerhoff , and Alexander J Summers . 2014 . Viper: A verification infrastructure for permission-based reasoning. ETH Zurich. Uri Juhasz, Ioannis T Kassios, Peter M\u00fcller, Milos Novacek, Malte Schwerhoff, and Alexander J Summers. 2014. Viper: A verification infrastructure for permission-based reasoning. ETH Zurich."},{"key":"e_1_2_1_25_1","volume-title":"Proceedings of the ACM on Programming Languages, 4, POPL","author":"Jung Ralf","year":"2019","unstructured":"Ralf Jung , Hoang-Hai Dang , Jeehoon Kang , and Derek Dreyer . 2019 . Stacked borrows: an aliasing model for Rust . Proceedings of the ACM on Programming Languages, 4, POPL (2019), 1\u201332. Ralf Jung, Hoang-Hai Dang, Jeehoon Kang, and Derek Dreyer. 2019. Stacked borrows: an aliasing model for Rust. Proceedings of the ACM on Programming Languages, 4, POPL (2019), 1\u201332."},{"key":"e_1_2_1_26_1","volume-title":"Proceedings of the ACM on Programming Languages, 2, POPL","author":"Jung Ralf","year":"2017","unstructured":"Ralf Jung , Jacques-Henri Jourdan , Robbert Krebbers , and Derek Dreyer . 2017 . RustBelt: Securing the foundations of the Rust programming language . Proceedings of the ACM on Programming Languages, 2, POPL (2017), 1\u201334. Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer. 2017. RustBelt: Securing the foundations of the Rust programming language. Proceedings of the ACM on Programming Languages, 2, POPL (2017), 1\u201334."},{"key":"e_1_2_1_27_1","volume-title":"Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Journal of Functional Programming, 28","author":"Jung Ralf","year":"2018","unstructured":"Ralf Jung , Robbert Krebbers , Jacques-Henri Jourdan , Ale\u0161 Bizjak , Lars Birkedal , and Derek Dreyer . 2018. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Journal of Functional Programming, 28 ( 2018 ). Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ale\u0161 Bizjak, Lars Birkedal, and Derek Dreyer. 2018. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Journal of Functional Programming, 28 (2018)."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3527313"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385971"},{"key":"e_1_2_1_32_1","unstructured":"Niko Matsakis. 2018. Regions are Sets of Loans. http:\/\/smallcultfollowing.com\/babysteps\/blog\/2018\/04\/27\/an-alias-based-formulation-of-the-borrow-checker\/ \t\t\t\t  Niko Matsakis. 2018. Regions are Sets of Loans. http:\/\/smallcultfollowing.com\/babysteps\/blog\/2018\/04\/27\/an-alias-based-formulation-of-the-borrow-checker\/"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523704"},{"key":"e_1_2_1_34_1","doi-asserted-by":"crossref","unstructured":"Yusuke Matsushita Takeshi Tsukada and Naoki Kobayashi. 2020. RustHorn: CHC-Based Verification for Rust Programs.. In ESOP. 484\u2013514. \t\t\t\t  Yusuke Matsushita Takeshi Tsukada and Naoki Kobayashi. 2020. RustHorn: CHC-Based Verification for Rust Programs.. In ESOP. 484\u2013514.","DOI":"10.1007\/978-3-030-44914-8_18"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21401-6_26"},{"key":"e_1_2_1_36_1","volume-title":"Cogent: uniqueness types and certifying compilation. Journal of Functional Programming, 31","author":"O\u2019Connor LIAM","year":"2021","unstructured":"LIAM O\u2019Connor , Zilin Chen , Christine Rizkallah , Vincent Jackson , Sidney Amani , Gerwin Klein , Toby Murray , Thomas Sewell , and Gabriele Keller . 2021. Cogent: uniqueness types and certifying compilation. Journal of Functional Programming, 31 ( 2021 ). LIAM O\u2019Connor, Zilin Chen, Christine Rizkallah, Vincent Jackson, Sidney Amani, Gerwin Klein, Toby Murray, Thomas Sewell, and Gabriele Keller. 2021. Cogent: uniqueness types and certifying compilation. Journal of Functional Programming, 31 (2021)."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3018610.3018624"},{"key":"e_1_2_1_38_1","unstructured":"Jonathan Protzenko. 2014. Mezzo: a typed language for safe effectful concurrent programs. Ph. D. Dissertation. Universit\u00e9 Paris Diderot-Paris 7. \t\t\t\t  Jonathan Protzenko. 2014. Mezzo: a typed language for safe effectful concurrent programs. Ph. D. Dissertation. Universit\u00e9 Paris Diderot-Paris 7."},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110261"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_2_1_41_1","unstructured":"Xavier Rival. 2011. Abstract Domains for the Static Analysis of Programs Manipulating Complex Data Structures. Habilitation \u00e0 diriger des recherches \u00c9cole Normale Sup\u00e9rieure. \t\t\t\t  Xavier Rival. 2011. Abstract Domains for the Static Analysis of Programs Manipulating Complex Data Structures. Habilitation \u00e0 diriger des recherches \u00c9cole Normale Sup\u00e9rieure."},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454036"},{"key":"e_1_2_1_43_1","unstructured":"The Rust Compiler Team. 2021. The Polonius Book. https:\/\/rust-lang.github.io\/polonius\/ \t\t\t\t  The Rust Compiler Team. 2021. The Polonius Book. https:\/\/rust-lang.github.io\/polonius\/"},{"key":"e_1_2_1_44_1","unstructured":"The Rust Compiler Team. 2022. Guide to rustc development. https:\/\/rustc-dev-guide.rust-lang.org\/borrow_check\/two_phase_borrows.html \t\t\t\t  The Rust Compiler Team. 2022. Guide to rustc development. https:\/\/rustc-dev-guide.rust-lang.org\/borrow_check\/two_phase_borrows.html"},{"key":"e_1_2_1_45_1","volume-title":"Region-based memory management. Information and computation, 132, 2","author":"Tofte Mads","year":"1997","unstructured":"Mads Tofte and Jean-Pierre Talpin . 1997. Region-based memory management. Information and computation, 132, 2 ( 1997 ), 109\u2013176. Mads Tofte and Jean-Pierre Talpin. 1997. Region-based memory management. Information and computation, 132, 2 (1997), 109\u2013176."},{"key":"e_1_2_1_46_1","volume-title":"Simple verification of rust programs via functional purification. Master\u2019s Thesis","author":"Ullrich Sebastian","unstructured":"Sebastian Ullrich . 2016. Simple verification of rust programs via functional purification. Master\u2019s Thesis , Karlsruher Institut f\u00fcr Technologie (KIT) . Sebastian Ullrich. 2016. Simple verification of rust programs via functional purification. Master\u2019s Thesis, Karlsruher Institut f\u00fcr Technologie (KIT)."},{"key":"e_1_2_1_47_1","unstructured":"Philip Wadler. 1990. Linear types can change the world!. In Programming concepts and methods. 3 5. \t\t\t\t  Philip Wadler. 1990. Linear types can change the world!. In Programming concepts and methods. 3 5."},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485522"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3547647","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3547647","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T18:43:29Z","timestamp":1750272209000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3547647"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,8,29]]},"references-count":48,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2022,8,29]]}},"alternative-id":["10.1145\/3547647"],"URL":"https:\/\/doi.org\/10.1145\/3547647","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,8,29]]},"assertion":[{"value":"2022-08-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}