{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T11:07:19Z","timestamp":1784200039392,"version":"3.55.0"},"reference-count":34,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,6,10]]},"abstract":"<jats:p>We propose a hybrid approach to end-to-end Rust verification where the proof effort is split into powerful automated verification of safe Rust and targeted semi-automated verification of unsafe Rust. To this end, we present Gillian-Rust, a proof-of-concept semi-automated verification tool built on top of the Gillian platform that can reason about type safety and functional correctness of unsafe code. Gillian-Rust automates a rich separation logic for real-world Rust, embedding the lifetime logic of RustBelt and the parametric prophecies of RustHornBelt, and is able to verify real-world Rust standard library code with only minor annotations and with verification times orders of magnitude faster than those of comparable tools. We link Gillian-Rust with Creusot, a state-of-the-art verifier for safe Rust, by providing a systematic encoding of unsafe code specifications that Creusot can use but cannot verify, demonstrating the feasibility of our hybrid approach.<\/jats:p>","DOI":"10.1145\/3729289","type":"journal-article","created":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T16:02:27Z","timestamp":1749830547000},"page":"970-992","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":11,"title":["A Hybrid Approach to Semi-automated Rust Verification"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9419-5387","authenticated-orcid":false,"given":"Sacha-\u00c9lie","family":"Ayoun","sequence":"first","affiliation":[{"name":"Imperial College London, London, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2530-8418","authenticated-orcid":false,"given":"Xavier","family":"Denis","sequence":"additional","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0400-7467","authenticated-orcid":false,"given":"Petar","family":"Maksimovi\u0107","sequence":"additional","affiliation":[{"name":"Nethermind, London, United Kingdom"},{"name":"Imperial College London, London, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4187-0585","authenticated-orcid":false,"given":"Philippa","family":"Gardner","sequence":"additional","affiliation":[{"name":"Imperial College London, London, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,6,13]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1145\/3428204"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1145\/3360573"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","unstructured":"Sacha-\u00c9lie Ayoun Xavier Denis Petar Maksimovi\u0107 and Philippa Gardner. 2025. Artifact: A Hybrid Approach to Semi-Automated Rust Verification. Zenodo. https:\/\/doi.org\/10.5281\/zenodo.15183201 10.5281\/zenodo.15183201","DOI":"10.5281\/zenodo.15183201"},{"key":"e_1_3_2_5_2","doi-asserted-by":"crossref","unstructured":"S.-\u00c9. Ayoun X. Denis P. Maksimovi\u0107 and P. Gardner. 2025. A Hybrid Approach to Semi-Automated Rust Verification (Extended Version). https:\/\/arxiv.org\/abs\/2403.15122","DOI":"10.1145\/3729289"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-13188-2_7"},{"key":"e_1_3_2_8_2","doi-asserted-by":"crossref","unstructured":"X. Denis and J.-H. Jourdan. 2023. Specifying and Verifying Higher-order Rust Iterators. In TACAS\u201923 (Lecture Notes in Computer Science). 93\u2013110.","DOI":"10.1007\/978-3-031-30820-8_9"},{"key":"e_1_3_2_9_2","doi-asserted-by":"crossref","unstructured":"X. Denis J.-H. Jourdan and C. March\u00e9. 2022. Creusot: A Foundry for the Deductive Verification of Rust Programs. In FMSE\u201922. 90\u2013105.","DOI":"10.1007\/978-3-031-17244-1_6"},{"key":"e_1_3_2_10_2","doi-asserted-by":"crossref","unstructured":"J. Fragoso Santos P. Maksimovi\u0107 S.-\u00c9. Ayoun and P. Gardner. 2020. Gillian Part I: A Multi-Language Platform for Symbolic Execution. In PLDI\u201920. 927\u2013942.","DOI":"10.1145\/3385412.3386014"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/3656422"},{"key":"e_1_3_2_12_2","unstructured":"Unsafe Code Guidelines Working Group. 2023. Structs and Tuples - Memory Layout - Unsafe Code Guidelines. https:\/\/github.com\/rust-lang\/unsafe-code-guidelines\/blob\/50f8ff4b6892f98740de3b375e4d4bda10b9da9f\/reference\/src\/layout\/structs-and-tuples.md Accessed: Nov. 16 2019."},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/3547647"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17164-2_21"},{"key":"e_1_3_2_15_2","unstructured":"R. Jung. 2016. The Scope of Unsafe. https:\/\/www.ralfj.de\/blog\/2016\/01\/09\/the-scope-of-unsafe.html Accessed: March 3rd 2025."},{"key":"e_1_3_2_16_2","unstructured":"R. Jung. 2018. Two Kinds of Invariants: Safety and Validity. https:\/\/www.ralfj.de\/blog\/2018\/08\/22\/two-kinds-of-invariants.html Accessed: June 19th 2023."},{"key":"e_1_3_2_17_2","first-page":"41:1","volume-title":"Proceedings of the ACM on Programming Languages","author":"Jung R.","year":"2019","unstructured":"R. Jung, H.-H. Dang, J. Kang, and D. Dreyer. 2019. Stacked Borrows: An Aliasing Model for Rust. Proceedings of the ACM on Programming Languages 4, POPL (2019), 41:1\u201341:32."},{"key":"e_1_3_2_18_2","first-page":"66:1","volume-title":"Proceedings of the ACM on Programming Languages","author":"Jung R.","year":"2017","unstructured":"R. Jung, J.-H. Jourdan, R. Krebbers, and D. Dreyer. 2017. RustBelt: Securing the Foundations of the Rust Programming Language. Proceedings of the ACM on Programming Languages 2, POPL (2017), 66:1\u201366:34."},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_2_20_2","first-page":"45:1","volume-title":"Proceedings of the ACM on Programming Languages","author":"Jung R.","year":"2019","unstructured":"R. Jung, R. Lepigre, G. Parthasarathy, M. Rapoport, A. Timany, D. Dreyer, and B. Jacobs. 2019. The Future is Ours: Prophecy Variables in Separation Logic. Proceedings of the ACM on Programming Languages 4, POPL (2019), 45:1\u201345:32."},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/3586037"},{"key":"e_1_3_2_22_2","unstructured":"N. Lehmann A. Geller N. Vazou and R. Jhala. 2022. Flux: Liquid Types for Rust. http:\/\/arxiv.org\/abs\/2207.04034"},{"key":"e_1_3_2_23_2","unstructured":"X. Leroy A. W. Appel S. Blazy and G. Stewart. 2012. The CompCert Memory Model Version 2. Technical Report. Inria. https:\/\/hal.inria.fr\/hal-00703441 Pages: 26."},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","unstructured":"A. L\u00f6\u00f6w D. Nantes-Sobrinho S.-\u00c9. Ayoun C. Cronj\u00e4ger P. Maksimovi\u0107 and P. Gardner. 2024. Compositional Symbolic Execution for Correctness and Incorrectness Reasoning. In ECOOP\u201924. 25:1\u201325:28. https:\/\/doi.org\/10.4230\/LIPIcs.ECOOP.2024.25 10.4230\/LIPIcs.ECOOP.2024.25","DOI":"10.4230\/LIPIcs.ECOOP.2024.25"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","unstructured":"A. L\u00f6\u00f6w D. Nantes-Sobrinho S.-\u00c9. Ayoun P. Maksimovi\u0107 and P. Gardner. 2024. Matching Plans for Frame Inference in Compositional Reasoning. In ECOOP\u201924. 26:1\u201326:20. https:\/\/doi.org\/10.4230\/LIPIcs.ECOOP.2024.26 10.4230\/LIPIcs.ECOOP.2024.26","DOI":"10.4230\/LIPIcs.ECOOP.2024.26"},{"key":"e_1_3_2_26_2","doi-asserted-by":"crossref","unstructured":"P. Maksimovi\u0107 S.-\u00c9. Ayoun J. Fragoso Santos and P. Gardner. 2021. Gillian Part II: Real-World Verification for JavaScript and C. In CAV\u201921. 827\u2013850.","DOI":"10.1007\/978-3-030-81688-9_38"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1145\/2692956.2663188"},{"key":"e_1_3_2_28_2","doi-asserted-by":"crossref","unstructured":"Y. Matsushita X. Denis J.-H. Jourdan and D. Dreyer. 2022. RustHornBelt: A Semantic Foundation for Functional Verification of Rust Programs with Unsafe Code. In PLDI\u201922. 841\u2013856.","DOI":"10.1145\/3519939.3523704"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1145\/3462205"},{"key":"e_1_3_2_30_2","unstructured":"N. Rahimi Foroushaani and B. Jacobs. 2022. Modular Formal Verification of Rust Programs with Unsafe Blocks. http:\/\/arxiv.org\/abs\/2212.12976"},{"key":"e_1_3_2_31_2","doi-asserted-by":"crossref","unstructured":"M. Sammler R. Lepigre R. Krebbers K. Memarian D. Dreyer and D. Garg. 2021. RefinedC: Automating the Foundational Verification of C Code with Refined Ownership Types. In PLDI\u201921. 158\u2013174.","DOI":"10.1145\/3453483.3454036"},{"key":"e_1_3_2_32_2","unstructured":"The Coq Team. 2023. The Coq Proof Assistant. https:\/\/coq.inria.fr\/ Accessed: Nov. 16th 2023."},{"key":"e_1_3_2_33_2","unstructured":"The Kani Team. 2023. How Open Source Projects are Using Kani to Write Better Software in Rust | AWS Open Source Blog. https:\/\/aws.amazon.com\/blogs\/opensource\/how-open-source-projects-are-using-kani-to-write-better-software-in-rust\/ Accessed: Nov. 13th 2023."},{"key":"e_1_3_2_34_2","unstructured":"The Rust Team. 2023. Rust Programming Language. https:\/\/www.rust-lang.org\/ Accessed: Nov. 16th 2023."},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/3735592"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3729289","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T10:07:35Z","timestamp":1784196455000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3729289"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,10]]},"references-count":34,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2025,6,10]]}},"alternative-id":["10.1145\/3729289"],"URL":"https:\/\/doi.org\/10.1145\/3729289","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,6,10]]},"assertion":[{"value":"2024-11-14","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-03-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-06-13","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}