{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,5]],"date-time":"2026-06-05T15:01:17Z","timestamp":1780671677468,"version":"3.54.1"},"reference-count":232,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2026,6,5]],"date-time":"2026-06-05T00:00:00Z","timestamp":1780617600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2026,6,30]]},"abstract":"<jats:p>Project Everest began at Microsoft Research in 2016, aiming to spur research in program verification to produce industrial-grade software. In collaboration with INRIA and Carnegie Mellon University, Project Everest\u2019s goal was to produce drop-in verified replacements of secure communications software used in the HTTPS ecosystem, including TLS, the underlying cryptography, and related subprotocols. Now, almost a decade later, we reflect on the project, sharing both its successes and failures, and look ahead to the next decade of program verification research.<\/jats:p>","DOI":"10.1145\/3805702","type":"journal-article","created":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T14:48:03Z","timestamp":1775832483000},"page":"1-64","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Project Everest: Perspectives from Developing Industrial-Grade High-Assurance Software"],"prefix":"10.1145","volume":"48","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6595-2756","authenticated-orcid":false,"given":"Danel","family":"Ahman","sequence":"first","affiliation":[{"name":"University of Tartu, Tartu, Estonia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3152-8997","authenticated-orcid":false,"given":"Karthikeyan","family":"Bhargavan","sequence":"additional","affiliation":[{"name":"INRIA, Le Chesnay, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0007-5973-6820","authenticated-orcid":false,"given":"Barry","family":"Bond","sequence":"additional","affiliation":[{"name":"Self Employed, Redmond, Washington, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5596-6828","authenticated-orcid":false,"given":"Jay","family":"Bosamiya","sequence":"additional","affiliation":[{"name":"Microsoft Research, Redmond, Washington, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-7485-1217","authenticated-orcid":false,"given":"Christopher","family":"Brzuska","sequence":"additional","affiliation":[{"name":"Aalto University, Aalto, Finland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2838-4144","authenticated-orcid":false,"given":"Antoine","family":"Delignat-Lavaud","sequence":"additional","affiliation":[{"name":"Microsoft UK Ltd\u2014Reading, Cambridge, United Kingdom of Great Britain and Northern\u00a0Ireland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6929-886X","authenticated-orcid":false,"given":"C\u00e9dric","family":"Fournet","sequence":"additional","affiliation":[{"name":"Microsoft UK Ltd.\u2014Reading, Cambridge, United Kingdom of Great Britain and Northern Ireland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2642-543X","authenticated-orcid":false,"given":"Aymeric","family":"Fromherz","sequence":"additional","affiliation":[{"name":"INRIA, Paris, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8336-5405","authenticated-orcid":false,"given":"Sydney","family":"Gibson","sequence":"additional","affiliation":[{"name":"ZeroRISC, Pittsburgh, Pennsylvania, 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, Redmond, Washington, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8919-8081","authenticated-orcid":false,"given":"C\u0103t\u0103lin","family":"Hri\u021bcu","sequence":"additional","affiliation":[{"name":"MPI-SP, Bochum, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8660-9663","authenticated-orcid":false,"given":"Markulf","family":"Kohlweiss","sequence":"additional","affiliation":[{"name":"University of Edinburgh, Edinburgh, United Kingdom of Great Britain and Northern Ireland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-5831-9991","authenticated-orcid":false,"given":"Guido","family":"Mart\u00ednez","sequence":"additional","affiliation":[{"name":"Microsoft Research, Redmond, Washington, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7718-7905","authenticated-orcid":false,"given":"Haobin","family":"Ni","sequence":"additional","affiliation":[{"name":"University of Washington, Seattle, Washington, 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, Pittsburgh, Pennsylvania, USA"}],"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 Corporation, Redmond, Washington, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4590-9712","authenticated-orcid":false,"given":"Tahina","family":"Ramananandro","sequence":"additional","affiliation":[{"name":"Microsoft Research, Redmond, Washington, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3283-8011","authenticated-orcid":false,"given":"Aseem","family":"Rastogi","sequence":"additional","affiliation":[{"name":"Microsoft Research India, Bengaluru, India"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2114-624X","authenticated-orcid":false,"given":"Exequiel","family":"Rivas","sequence":"additional","affiliation":[{"name":"Tallinn University of Technology, Tallinn, Estonia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9254-3015","authenticated-orcid":false,"given":"Nikhil","family":"Swamy","sequence":"additional","affiliation":[{"name":"Microsoft Research, Redmond, Washington, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0479-9967","authenticated-orcid":false,"given":"Santiago","family":"Zanella-B\u00e9guelin","sequence":"additional","affiliation":[{"name":"Microsoft UK Ltd.\u2014Reading, Cambridge, United Kingdom of Great Britain and Northern Ireland"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,6,5]]},"reference":[{"key":"e_1_3_2_2_2","unstructured":"curve25519-donna. 2008. Implementations of a Fast Elliptic-Curve Diffie-Hellman Primitive. Retrieved from https:\/\/github.com\/agl\/curve25519-donna"},{"key":"e_1_3_2_3_2","unstructured":"The Sodium Crypto. 2013. Library (Libsodium). Retrieved from https:\/\/github.com\/jedisct1\/libsodium"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1109\/CSF51468.2021.00048"},{"key":"e_1_3_2_5_2","volume-title":"Proceedings of the International Conference on Cryptographic Hardware and Embedded Systems (CHES)","author":"Acii\u00e7mez Onur","year":"2010","unstructured":"Onur Acii\u00e7mez, Billy Bob Brumley, and Philipp Grabher. 2010. New results on instruction cache attacks. In Proceedings of the International Conference on Cryptographic Hardware and Embedded Systems (CHES)."},{"key":"e_1_3_2_6_2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3158153","article-title":"Recalling a witness: Foundations and applications of monotonic state","volume":"2","author":"Ahman Danel","year":"2017","unstructured":"Danel Ahman, C\u00e9dric Fournet, C\u0103t\u0103lin Hri\u0163cu, Kenji Maillard, Aseem Rastogi, and Nikhil Swamy. 2017. Recalling a witness: Foundations and applications of monotonic state. Proceedings of the ACM on Programming Languages 2, POPL (December 2017), 1\u201330.","journal-title":"Proceedings of the ACM on Programming Languages"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/3093333.3009878"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2010.27"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134078"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-35672-3_1"},{"key":"e_1_3_2_11_2","unstructured":"Daneshvar Amrollahi Mathias Preiner Aina Niemetz Andrew Reynolds Moses Charikar Cesare Tinelli and Clark Barrett. 2024. Using normalization to improve SMT solver stability. arXiv:2410.22419. Retrieved from https:\/\/arxiv.org\/abs\/2410.22419"},{"key":"e_1_3_2_12_2","unstructured":"Cezar-Constantin Andrici Danel Ahman C\u0103t\u0103lin Hri\u0163cu Ruxandra Icleanu Guido Mart\u00ednez Exequiel Rivas and Th\u00e9o Winterhalter. 2025. SecRef*: Securely sharing mutable references between verified and unverified code in F*. arXiv:2503.00404. Retrieved from https:\/\/arxiv.org\/abs\/2503.00404"},{"key":"e_1_3_2_13_2","first-page":"2226","volume-title":"Proceedings of the ACM on Programming Languages","volume":"8","author":"Andrici Cezar-Constantin","year":"2024","unstructured":"Cezar-Constantin Andrici, \u015etefan Ciob\u00e2c\u0103, Catalin Hritcu, Guido Mart\u00ednez, Exequiel Rivas, \u00c9ric Tanter, and Th\u00e9o Winterhalter. 2024. Securing verified IO programs against unverified code in F \\({}^{\\star}\\) . Proceedings of the ACM on Programming Languages 8, POPL (2024), 2226\u20132259."},{"key":"e_1_3_2_14_2","unstructured":"Cezar-Constantin Andrici Th\u00e9o Winterhalter C\u0103t\u0103lin Hri\u0163cu and Exequiel Rivas. 2022. Verifying non-terminating programs with IO in F*. Presentation at the 10th ACM SIGPLAN Workshop on Higher-Order Programming with Effects (HOPE)."},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2015.44"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/2701415"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1145\/3573105.3575687"},{"key":"e_1_3_2_18_2","unstructured":"Arm. 2025. NEON Instructions. Retrieved March 2025 from https:\/\/developer.arm.com\/documentation\/dui0473\/m\/neon-instructions"},{"key":"e_1_3_2_19_2","first-page":"615","volume-title":"Proceedings of the 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Bangert Julian","year":"2014","unstructured":"Julian Bangert and Nickolai Zeldovich. 2014. Nail: A practical tool for parsing and generating data formats. In Proceedings of the 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI), 615\u2013628."},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/3587692"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00008"},{"key":"e_1_3_2_22_2","doi-asserted-by":"crossref","unstructured":"Richard Barnes Benjamin Beurdouche Raphael Robert Jon Millican Emad Omara and Katriel Cohn-Gordon. 2023. The Messaging Layer Security (MLS) Protocol. RFC Editor. Retrieved from https:\/\/www.rfc-editor.org\/info\/rfc9420","DOI":"10.17487\/RFC9420"},{"key":"e_1_3_2_23_2","doi-asserted-by":"crossref","unstructured":"Richard Barnes Karthikeyan Bhargavan Benjamin Lipp and Christopher A. Wood. 2022. Hybrid Public Key Encryption. RFC Editor. Retrieved from https:\/\/www.rfc-editor.org\/info\/rfc9180","DOI":"10.17487\/RFC9180"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22792-9_5"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/1890028.1890031"},{"key":"e_1_3_2_26_2","first-page":"115","volume-title":"Proceedings of the 4th International Symposium on Formal Methods for Components and Objects (FMCO \u201905), Revised Lectures","author":"Berdine Josh","year":"2005","unstructured":"Josh Berdine, Cristiano Calcagno, and Peter W. O\u2019Hearn. 2005. Smallfoot: Modular automatic assertion checking with separation logic. In Proceedings of the 4th International Symposium on Formal Methods for Components and Objects (FMCO \u201905), Revised Lectures. Frank S. de Boer, Marcello M. Bonsangue, Susanne Graf, and Willem P. de Roever (Eds.), Lecture Notes in Computer Science, Vol. 4111, Springer, 115\u2013137."},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1007\/11575467_5"},{"key":"e_1_3_2_28_2","volume-title":"Proceedings of the USENIX Security Symposium","author":"Beringer Lennart","year":"2015","unstructured":"Lennart Beringer, Adam Petcher, Katherine Q. Ye, and Andrew W. Appel. 2015. Verified correctness and security of OpenSSL HMAC. In Proceedings of the USENIX Security Symposium."},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1007\/11745853_14"},{"key":"e_1_3_2_30_2","unstructured":"Daniel J. Bernstein. 2019. Public-Key Authenticated Encryption: Crypto_box. Retrieved from https:\/\/nacl.cr.yp.to\/box.html"},{"key":"e_1_3_2_31_2","unstructured":"Daniel J. Bernstein. 2005. Cache-Timing Attacks on AES. Retrieved from https:\/\/cr.yp.to\/papers.html#cachetiming"},{"key":"e_1_3_2_32_2","unstructured":"Daniel J. Bernstein Karthikeyan Bhargavan Shivam Bhasin Anupam Chattopadhyay Tee Kiah Chia Matthias J. Kannwischer Franziskus Kiefer Thales B. Paiva Prasanna Ravi and Goutam Tamvada. 2024. KyberSlash: Exploiting secret-dependent division timings in Kyber implementations. IACR Cryptology ePrint Archive 1049. Retrieved from https:\/\/eprint.iacr.org\/2024\/1049"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1109\/EuroSP51992.2021.00042"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","unstructured":"Karthikeyan Bhargavan Abhishek Bichhawat Quoc Huy Do Pedram Hosseyni Ralf K\u00fcsters Guido Schmitz and Tim W\u00fcrtele. 2021. An in-depth symbolic security analysis of the ACME standard. In Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security. Association for Computing Machinery. DOI: 10.1145\/3460120.3484588","DOI":"10.1145\/3460120.3484588"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-91631-2_4"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2017.26"},{"key":"e_1_3_2_37_2","first-page":"1","volume-title":"Proceedings of the 2nd Summit on Advances in Programming Languages (SNAPL \u201917)","volume":"1","author":"Bhargavan Karthikeyan","year":"2017","unstructured":"Karthikeyan Bhargavan, Barry Bond, Antoine Delignat-Lavaud, C\u00e9dric Fournet, Chris Hawblitzel, Catalin Hritcu, Samin Ishtiaq, Markulf Kohlweiss, K. Rustan M. Leino, Jay R. Lorch, et al. 2017. Everest: Towards a verified, drop-in replacement of HTTPS. In Proceedings of the 2nd Summit on Advances in Programming Languages (SNAPL \u201917). Benjamin S. Lerner, Rastislav Bod\u00edk, and Shriram Krishnamurthi (Eds.), LIPIcs, Vol. 71, Schloss Dagstuhl\u2014Leibniz-Zentrum f\u00fcr Informatik, Article 1, 1\u201312."},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2016.37"},{"key":"e_1_3_2_39_2","doi-asserted-by":"crossref","unstructured":"Karthikeyan Bhargavan Maxime Buyse Lucas Franceschino Lasse Letager Hansen Franziskus Kiefer Jonas Schneider-Bensch and Bas Spitters. 2025. HAX: Verifying security-critical Rust software using multiple provers. In Verified Software. Theories Tools and Experiments. Jonathan Protzenko and Azalea Raad (Eds.) Springer Nature Switzerland Cham 96\u2013119.","DOI":"10.1007\/978-3-031-86695-1_7"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2013.37"},{"key":"e_1_3_2_41_2","unstructured":"Karthikeyan Bhargavan Lucas Franceschino Franziskus Kiefer and Goutam Tamvada. 2024. Verifying Libcrux\u2019s ML-KEM. Retrieved from https:\/\/cryspen.com\/post\/ml-kem-verification\/"},{"key":"e_1_3_2_42_2","doi-asserted-by":"crossref","unstructured":"Karthikeyan Bhargavan Lasse Letager Hansen Franziskus Kiefer Jonas Schneider-Bensch and Bas Spitters. 2025. Formal security and functional verification of cryptographic protocol implementations in Rust. Cryptology ePrint Archive Paper 2025\/980. Retrieved from https:\/\/eprint.iacr.org\/2025\/980","DOI":"10.1145\/3719027.3765213"},{"key":"e_1_3_2_43_2","doi-asserted-by":"crossref","unstructured":"Henk Birkholz Christoph Vigano and Carsten Bormann. 2019. Concise Data Definition Language (CDDL): A Notational Convention to Express Concise Binary Object Representation (CBOR) and JSON Data Structures. RFC Editor. Retrieved from https:\/\/www.rfc-editor.org\/info\/rfc8610","DOI":"10.17487\/RFC8610"},{"key":"e_1_3_2_44_2","first-page":"54","volume-title":"Foundations of Security Analysis and Design VII\u2014FOSAD 2012\/2013 Tutorial Lectures","author":"Blanchet Bruno","year":"2013","unstructured":"Bruno Blanchet. 2013. Automatic verification of security protocols in the symbolic model: The verifier ProVerif. In Foundations of Security Analysis and Design VII\u2014FOSAD 2012\/2013 Tutorial Lectures. Alessandro Aldini, Javier L\u00f3pez, and Fabio Martinelli (Eds.), Lecture Notes in Computer Science, Vol. 8604, Springer, 54\u201387."},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","DOI":"10.5555\/2032266.2032277"},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14052-5_14"},{"key":"e_1_3_2_47_2","volume-title":"Proceedings of the USENIX Security Symposium","author":"Bond Barry","year":"2017","unstructured":"Barry Bond, Chris Hawblitzel, Manos Kapritsos, K. Rustan, M. Leino, Jacob R. Lorch, Bryan Parno, Ashay Rane, Srinath Setty, and Laure Thompson. 2017. Vale: Verifying high-performance cryptographic assembly code. In Proceedings of the USENIX Security Symposium."},{"key":"e_1_3_2_48_2","doi-asserted-by":"crossref","unstructured":"Carsten Bormann and Paul E. Hoffman. 2020. Concise Binary Object Representation (CBOR). RFC Editor. Retrieved from https:\/\/www.rfc-editor.org\/info\/rfc8949","DOI":"10.17487\/RFC8949"},{"key":"e_1_3_2_49_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-63618-0_7"},{"key":"e_1_3_2_50_2","volume-title":"Proceedings of the USENIX Security Symposium","author":"Bosamiya Jay","year":"2022","unstructured":"Jay Bosamiya, Wen Shih Lim, and Bryan Parno., August. 2022. Provably-safe multilingual software sandboxing using WebAssembly. In Proceedings of the USENIX Security Symposium."},{"key":"e_1_3_2_51_2","volume-title":"Proceedings of the USENIX Security Symposium","author":"Brumley David","year":"2003","unstructured":"David Brumley and Dan Boneh., August. 2003. Remote timing attacks are practical. In Proceedings of the USENIX Security Symposium."},{"key":"e_1_3_2_52_2","doi-asserted-by":"publisher","unstructured":"Chris Brzuska Antoine Delignat-Lavaud Christoph Egger C\u00e9dric Fournet Konrad Kohbrok and Markulf Kohlweiss. 2022. Key-schedule security for the TLS 1.3 standard. In Advances in Cryptology \u2013 ASIACRYPT 2022: 28th International Conference on the Theory and Application of Cryptology and Information Security Taipei Taiwan December 5\u20139 2022 Proceedings Part I. Springer-Verlag Berlin 621\u2013650. DOI: 10.1007\/978-3-031-22963-3_21","DOI":"10.1007\/978-3-031-22963-3_21"},{"key":"e_1_3_2_53_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP46214.2022.9833678"},{"key":"e_1_3_2_54_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-22963-3_21"},{"key":"e_1_3_2_55_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-03332-3_9"},{"key":"e_1_3_2_56_2","unstructured":"Chris Brzuska Christoph Egger and Jan Winkelmann. 2025. SSBee. Retrieved from https:\/\/github.com\/sspverif\/sspverif\/"},{"key":"e_1_3_2_57_2","first-page":"137","volume-title":"Proceedings of the 36th IEEE Computer Security Foundations Symposium (CSF)","author":"Brzuska Chris","year":"2023","unstructured":"Chris Brzuska and Sabine Oechsner. 2023. A state-separating proof for Yao\u2019s garbling scheme. In Proceedings of the 36th IEEE Computer Security Foundations Symposium (CSF). IEEE, 137\u2013152."},{"key":"e_1_3_2_58_2","volume-title":"Proceedings of the USENIX Security Symposium","author":"Cai Yi","year":"2025","unstructured":"Yi Cai, Pratap Singh, Zhengyao Lin, Jay Bosamiya, Joshua Gancher, Milijana Surbatovich, and Bryan Parno. 2025. Vest: Verified, secure, high-performance parsing and serialization for Rust. In Proceedings of the USENIX Security Symposium."},{"key":"e_1_3_2_59_2","first-page":"1365","volume-title":"Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security (CCS \u201916","author":"Calzavara Stefano","year":"2016","unstructured":"Stefano Calzavara, Alvise Rabitti, and Michele Bugliesi. 2016. Content security problems? Evaluating the effectiveness of content security policy in the wild. In Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security (CCS \u201916). ACM, New York, NY, 1365\u20131375."},{"key":"e_1_3_2_60_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE55347.2025.00002"},{"key":"e_1_3_2_61_2","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/2023.findings-emnlp.614"},{"key":"e_1_3_2_62_2","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806643"},{"key":"e_1_3_2_63_2","doi-asserted-by":"publisher","DOI":"10.1145\/3625275.3625401"},{"key":"e_1_3_2_64_2","doi-asserted-by":"publisher","DOI":"10.1145\/2660267.2660370"},{"key":"e_1_3_2_65_2","doi-asserted-by":"crossref","unstructured":"D. Cooper S. Santesson S. Farrell S. Boeyen R. Housley and W. Polk. 2008. RFC 5280: Internet X.509 public key infrastructure certificate and certificate revocation list (CRL) profile.","DOI":"10.17487\/rfc5280"},{"key":"e_1_3_2_66_2","doi-asserted-by":"publisher","DOI":"10.5555\/993868"},{"key":"e_1_3_2_67_2","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908100"},{"key":"e_1_3_2_68_2","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134063"},{"key":"e_1_3_2_69_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2016.35"},{"key":"e_1_3_2_70_2","unstructured":"DARPA. 2024. Translating All C to Rust (TRACTOR). Retrieved September 2024 from https:\/\/www.darpa.mil\/program\/translating-all-c-to-rust"},{"key":"e_1_3_2_71_2","volume-title":"Proceedings of the 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 of the Conference on Automated Deduction (CADE)."},{"key":"e_1_3_2_72_2","first-page":"337","volume-title":"Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"Mendon\u00e7a de Moura Leonardo","year":"2008","unstructured":"Leonardo Mendon\u00e7a de Moura and Nikolaj Bj\u00f8rner. 2008. Z3: An efficient SMT solver. In Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Lecture Notes in Computer Science, Vol. 4963, Springer, 337\u2013340."},{"key":"e_1_3_2_73_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2017.58"},{"key":"e_1_3_2_74_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00039"},{"key":"e_1_3_2_75_2","volume-title":"Proceedings of the International Conference on Formal Engineering Methods","author":"Denis Xavier","year":"2022","unstructured":"Xavier Denis, Jacques-Henri Jourdan, and Claude March\u00e9. 2022. Creusot: A foundry for the deductive verification of Rust programs. In Proceedings of the International Conference on Formal Engineering Methods."},{"key":"e_1_3_2_76_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-48869-1_5"},{"key":"e_1_3_2_77_2","doi-asserted-by":"crossref","unstructured":"Jason A. Donenfeld. 2017. Wireguard: Next Generation Kernel Network Tunnel. Retrieved January 2017 from https:\/\/www.wireguard.com\/","DOI":"10.14722\/ndss.2017.23160"},{"key":"e_1_3_2_78_2","unstructured":"Jason A. Donenfeld. 2018. New 25519 Measurements of Formally Verified Implementations. Retrieved February 2018 from http:\/\/moderncrypto.org\/mail-archive\/curves\/2018\/000972.html"},{"key":"e_1_3_2_79_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00145-021-09387-y"},{"key":"e_1_3_2_80_2","doi-asserted-by":"publisher","DOI":"10.1109\/CSF54842.2022.9919671"},{"key":"e_1_3_2_81_2","doi-asserted-by":"publisher","DOI":"10.1145\/3729311"},{"key":"e_1_3_2_82_2","unstructured":"Christoph Egger. 2023. On Abstraction and Modularization in Protocol Analysis. Doctoral thesis. Friedrich-Alexander-Universit\u00e4t Erlangen-N\u00fcrnberg (FAU)."},{"key":"e_1_3_2_83_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-98668-0_5"},{"key":"e_1_3_2_84_2","first-page":"21","article-title":"Extending SMTCoq, a certified checker for SMT (extended abstract)","volume":"210","author":"Ekici Burak","year":"2016","unstructured":"Burak Ekici, Guy Katz, Chantal Keller, Alain Mebsout, Andrew J. Reynolds, and Cesare Tinelli. 2016. Extending SMTCoq, a certified checker for SMT (extended abstract). In Proceedings 1st International Workshop on Hammers for Type Theories (HaTT@IJCAR \u201916). Jasmin Christian Blanchette and Cezary Kaliszyk (Eds.), EPTCS, Vol. 210, 21\u201329.","journal-title":"Proceedings 1st International Workshop on Hammers for Type Theories (HaTT@IJCAR \u201916)"},{"key":"e_1_3_2_85_2","doi-asserted-by":"publisher","DOI":"10.1145\/3660791"},{"key":"e_1_3_2_86_2","volume-title":"Proceedings of the IEEE Symposium on Security and Privacy","author":"Erbsen A.","year":"2019","unstructured":"A. Erbsen, J. Philipoom, J. Gross, R. Sloan, and A. Chlipala. 2019. Simple high-level code for cryptographic arithmetic\u2014with proofs, without compromises. In Proceedings of the IEEE Symposium on Security and Privacy."},{"key":"e_1_3_2_87_2","doi-asserted-by":"publisher","DOI":"10.1145\/3656446"},{"key":"e_1_3_2_88_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE55347.2025.00173"},{"key":"e_1_3_2_89_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2013.42"},{"key":"e_1_3_2_90_2","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132782"},{"key":"e_1_3_2_91_2","doi-asserted-by":"publisher","DOI":"10.1145\/3611643.3616243"},{"key":"e_1_3_2_92_2","doi-asserted-by":"publisher","DOI":"10.1145\/3656444"},{"key":"e_1_3_2_93_2","doi-asserted-by":"publisher","DOI":"10.1145\/2046707.2046746"},{"key":"e_1_3_2_94_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290376"},{"key":"e_1_3_2_95_2","unstructured":"Aymeric Fromherz and Jonathan Protzenko. 2024. Compiling C to safe Rust formalized. arXiv:2412.15042. Retrieved from https:\/\/arxiv.org\/abs\/2412.15042"},{"key":"e_1_3_2_96_2","doi-asserted-by":"publisher","DOI":"10.1145\/3473590"},{"issue":"5","key":"e_1_3_2_97_2","first-page":"45","article-title":"Partial evaluation of computation process-an approach to a compiler-compiler","volume":"2","author":"Futamura Yoshihiko","year":"1971","unstructured":"Yoshihiko Futamura. 1971. Partial evaluation of computation process-an approach to a compiler-compiler. Systems, Computers, Controls 2, 5 (1971), 45\u201350.","journal-title":"Systems, Computers, Controls"},{"key":"e_1_3_2_98_2","doi-asserted-by":"publisher","DOI":"10.1145\/3656422"},{"key":"e_1_3_2_99_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP46215.2023.10179477"},{"key":"e_1_3_2_100_2","unstructured":"Google. 2022. Announcing KataOS and Sparrow. Retrieved October 2022 from https:\/\/opensource.googleblog.com\/2022\/10\/announcing-kataos-and-sparrow.html"},{"key":"e_1_3_2_101_2","doi-asserted-by":"publisher","DOI":"10.1145\/3167090"},{"key":"e_1_3_2_102_2","doi-asserted-by":"publisher","DOI":"10.1145\/3656439"},{"key":"e_1_3_2_103_2","first-page":"653","volume-title":"Proceedings of the 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI \u201916)","author":"Gu Ronghui","year":"2016","unstructured":"Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan (Newman) Wu, Jieung Kim, Vilhelm Sj\u00f6berg, and David Costanzo. 2016. CertiKOS: An extensible architecture for building certified concurrent OS kernels. In Proceedings of the 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI \u201916). USENIX Association, 653\u2013669."},{"key":"e_1_3_2_104_2","unstructured":"Shay Gueron. 2012. Intel\u00ae Advanced Encryption Standard (AES) New Instructions Set. Retrieved September 2012 from https:\/\/software.intel.com\/sites\/default\/files\/article\/165683\/aes-wp-2012-09-22-v01.pdf"},{"key":"e_1_3_2_105_2","unstructured":"Sean Gulley Vinodh Gopal Kirk Yap Wajdi Feghali Jim Guilford and Gil Wolrich. 2013. Intel\u00ae SHA Extensions. Retrieved July 2013 from https:\/\/software.intel.com\/sites\/default\/files\/article\/402097\/intel-sha-extensions-white-paper.pdf"},{"key":"e_1_3_2_106_2","doi-asserted-by":"publisher","DOI":"10.1145\/3140587.3062363"},{"key":"e_1_3_2_107_2","doi-asserted-by":"publisher","DOI":"10.1145\/3636501.3636961"},{"key":"e_1_3_2_108_2","doi-asserted-by":"publisher","DOI":"10.1145\/3594735"},{"key":"e_1_3_2_109_2","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815428"},{"key":"e_1_3_2_110_2","volume-title":"Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI)","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 Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI)."},{"key":"e_1_3_2_111_2","doi-asserted-by":"publisher","DOI":"10.1145\/3607844"},{"key":"e_1_3_2_112_2","doi-asserted-by":"publisher","DOI":"10.1145\/3547647"},{"key":"e_1_3_2_113_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP46214.2022.9833621"},{"key":"e_1_3_2_114_2","doi-asserted-by":"publisher","DOI":"10.1145\/3658644.3690263"},{"key":"e_1_3_2_115_2","doi-asserted-by":"publisher","DOI":"10.1109\/52.991327"},{"key":"e_1_3_2_116_2","doi-asserted-by":"publisher","DOI":"10.1145\/1925844.1926402"},{"key":"e_1_3_2_117_2","doi-asserted-by":"publisher","DOI":"10.5555\/647555.729729"},{"key":"e_1_3_2_118_2","unstructured":"Intel. 2014. New instructions supporting large integer arithmetic on Intel Architecture processors. Retrieved from https:\/\/raw.githubusercontent.com\/wiki\/intel\/intel-ipsec-mb\/doc\/ia-large-integer-arithmetic-paper.pdf"},{"key":"e_1_3_2_119_2","unstructured":"ITU Recommendation X 680. 2021. ITU-T study group 17. X.680: Information technology\u2014Abstract syntax notation one (ASN.1): Specification of basic notation. Retrieved from https:\/\/standards.globalspec.com\/std\/14381752\/x-680"},{"key":"e_1_3_2_120_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_4"},{"key":"e_1_3_2_121_2","first-page":"275","volume-title":"Proceedings of the General Track of the Annual Conference on USENIX Annual Technical Conference (ATEC \u201902)","author":"Jim Trevor","year":"2002","unstructured":"Trevor Jim, J. Greg Morrisett, Dan Grossman, Michael W. Hicks, James Cheney, and Yanling Wang. 2002. Cyclone: A safe dialect of C. In Proceedings of the General Track of the Annual Conference on USENIX Annual Technical Conference (ATEC \u201902). USENIX Association, 275\u2013288."},{"key":"e_1_3_2_122_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_2_123_2","unstructured":"Ben Kallus Prashant Anantharaman Michael Locasto and Sean W. Smith. 2024. The HTTP garden: Discovering parsing vulnerabilities in HTTP\/1.1 implementations by differential fuzzing of request streams."},{"key":"e_1_3_2_124_2","unstructured":"Adharsh Kamath Aditya Senthilnathan Saikat Chakraborty Pantazis Deligiannis Shuvendu K. Lahiri Akash Lal Aseem Rastogi Subhajit Roy and Rahul Sharma. 2023. Finding inductive loop invariants using large language models. arXiv:2311.07948. Retrieved from https:\/\/arxiv.org\/abs\/2311.07948"},{"key":"e_1_3_2_125_2","doi-asserted-by":"publisher","DOI":"10.1007\/11813040_19"},{"key":"e_1_3_2_126_2","unstructured":"Franziskus Kiefer and Karthikeyan Bhargavan. 2024. Formally Verified Post-Quantum Cryptography. Retrieved August 2024 from https:\/\/cryspen.com\/post\/fospqc\/"},{"key":"e_1_3_2_127_2","doi-asserted-by":"publisher","DOI":"10.1145\/2560537"},{"key":"e_1_3_2_128_2","unstructured":"Konrad Kobrok Markulf Kohlweiss Tahina Ramananandro and Nikhil Swamy. 2020. Relational F* for State Separating Cryptographic Proofs. Retrieved January 2020 from https:\/\/github.com\/FStarLang\/FStar\/wiki\/Relational-F*-for-State-Separating-Cryptographic-Proofs"},{"key":"e_1_3_2_129_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2019.00002"},{"key":"e_1_3_2_130_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-68697-5_9"},{"key":"e_1_3_2_131_2","unstructured":"Konrad Kohbrok. 2023. State-Separating Proofs and Their Applications. Doctoral thesis Aalto University School of Science."},{"key":"e_1_3_2_132_2","doi-asserted-by":"publisher","DOI":"10.1145\/3729310"},{"key":"e_1_3_2_133_2","doi-asserted-by":"publisher","DOI":"10.1145\/3664646.3676274"},{"key":"e_1_3_2_134_2","first-page":"26337","article-title":"Hypertree proof search for neural theorem proving","volume":"35","author":"Lample Guillaume","year":"2022","unstructured":"Guillaume Lample, Timothee Lacroix, Marie-Anne Lachaux, Aurelien Rodriguez, Amaury Hayat, Thibaut Lavril, Gabriel Ebner, and Xavier Martinet. 2022. Hypertree proof search for neural theorem proving. In Proceedings of the Advances in Neural Information Processing Systems, Vol. 35, 26337\u201326349.","journal-title":"Proceedings of the Advances in Neural Information Processing Systems"},{"key":"e_1_3_2_135_2","doi-asserted-by":"publisher","DOI":"10.1145\/279227.279229"},{"key":"e_1_3_2_136_2","doi-asserted-by":"publisher","DOI":"10.1145\/3098822.3098842"},{"key":"e_1_3_2_137_2","doi-asserted-by":"publisher","DOI":"10.1145\/3694715.3695952"},{"key":"e_1_3_2_138_2","doi-asserted-by":"publisher","DOI":"10.1145\/3586037"},{"key":"e_1_3_2_139_2","doi-asserted-by":"publisher","DOI":"10.1145\/3591283"},{"key":"e_1_3_2_140_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_20"},{"key":"e_1_3_2_141_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_3_2_142_2","volume-title":"Proceedings of the Conference on Verified Software: Theories, Tools, Experiments (VSTTE)","author":"Rustan K.","year":"2014","unstructured":"K. Rustan, M. Leino, and Nadia Polikarpova. 2014. Verified calculations. In Proceedings of the Conference on Verified Software: Theories, Tools, Experiments (VSTTE)."},{"key":"e_1_3_2_143_2","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111042"},{"key":"e_1_3_2_144_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69407-6_39"},{"key":"e_1_3_2_145_2","doi-asserted-by":"publisher","DOI":"10.1145\/3622849"},{"key":"e_1_3_2_146_2","unstructured":"Chang Liu Xiwei Wu Yuan Feng Qinxiang Cao and Junchi Yan. 2023. Towards general loop invariant generation via coordinating symbolic execution and large language models. arXiv:2311.10483. Retrieved from https:\/\/arxiv.org\/abs\/2311.10483"},{"key":"e_1_3_2_147_2","doi-asserted-by":"publisher","DOI":"10.1145\/3456629"},{"key":"e_1_3_2_148_2","doi-asserted-by":"publisher","DOI":"10.1145\/3341708"},{"key":"e_1_3_2_149_2","doi-asserted-by":"publisher","DOI":"10.1145\/3371072"},{"key":"e_1_3_2_150_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17184-1_2"},{"key":"e_1_3_2_151_2","unstructured":"L\u00fac\u00e1s C. Meier. 2022. State Separable Proofs for the Curious Cryptographer. Blogpost. Retrieved from https:\/\/cronokirby.com\/posts\/2022\/05\/state-separable-proofs-for-the-curious-cryptographer\/"},{"key":"e_1_3_2_152_2","unstructured":"Microsoft. 2023. Rust for Windows and the Windows Crate. Retrieved August 2023 from https:\/\/learn.microsoft.com\/en-us\/windows\/dev-environment\/rust\/rust-for-windows"},{"key":"e_1_3_2_153_2","unstructured":"Shane Miller and Carl Lerche. 2022. Sustainability with Rust. Retrieved February 2022 from https:\/\/aws.amazon.com\/blogs\/opensource\/sustainability-with-rust\/"},{"key":"e_1_3_2_154_2","unstructured":"Mozilla. 2018. Measurement Dashboard. Retrieved July 2018 from https:\/\/mzl.la\/2ug9YCH"},{"key":"e_1_3_2_155_2","unstructured":"Mozilla. 2021. Mozilla Welcomes the Rust Foundation. Retrieved February 2021 from https:\/\/blog.mozilla.org\/en\/mozilla\/mozilla-welcomes-the-rust-foundation\/"},{"key":"e_1_3_2_156_2","unstructured":"National Institute of Standards and Technology. 2012. Secure Hash Standard (SHS). FIPS PUB 180\u20134."},{"key":"e_1_3_2_157_2","doi-asserted-by":"publisher","DOI":"10.1145\/3573105.3575684"},{"key":"e_1_3_2_158_2","unstructured":"NIST. 2001. Recommendation for Block Cipher Modes of Operation: Methods and Techniques. NIST Special Publication 800-38A."},{"key":"e_1_3_2_159_2","unstructured":"NIST. 2001. Announcing the Advanced Encryption Standard (AES). Federal Information Processing Standards Publication 197."},{"key":"e_1_3_2_160_2","unstructured":"NIST. 2007. Recommendation for Block Cipher Modes of Operation: Galois\/Counter Mode (GCM) and GMAC. NIST Special Publication 800-38D."},{"key":"e_1_3_2_161_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-28644-8_4"},{"key":"e_1_3_2_162_2","doi-asserted-by":"publisher","DOI":"10.1145\/3503222.3507729"},{"key":"e_1_3_2_163_2","volume-title":"Proceedings of Selected Areas in Cryptography (SAC)","author":"Oliveira Thomaz","year":"2017","unstructured":"Thomaz Oliveira, Julio L\u00f3pez, H\u00fcseyin H\u0131\u015f\u0131l, Armando Faz-Hern\u00e1ndez, and Francisco Rodr\u00edguez-Henr\u00edquez. 2017. How to (pre-)compute a ladder: Improving the performance of X25519 and X448. In Proceedings of Selected Areas in Cryptography (SAC)."},{"key":"e_1_3_2_164_2","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523703"},{"key":"e_1_3_2_165_2","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062347"},{"key":"e_1_3_2_166_2","doi-asserted-by":"publisher","DOI":"10.1145\/3610721"},{"key":"e_1_3_2_167_2","doi-asserted-by":"publisher","DOI":"10.5555\/3618408.3619552"},{"key":"e_1_3_2_168_2","unstructured":"Colin Percival. 2005. Cache Missing for Fun and Profit. Retrieved from https:\/\/papers.freebsd.org\/2005\/cperciva-cache_missing\/"},{"key":"e_1_3_2_169_2","doi-asserted-by":"publisher","DOI":"10.1145\/3372297.3423352"},{"key":"e_1_3_2_170_2","volume-title":"Proceedings of the Conference on Concurrency Theory (CONCUR)","author":"Polyakov Andy","year":"2018","unstructured":"Andy Polyakov, Ming-Hsien Tsai, Bow-Yaw Wang, and Bo-Yin Yang. 2018. Verifying arithmetic assembly programs in cryptographic primitives. In Proceedings of the Conference on Concurrency Theory (CONCUR)."},{"key":"e_1_3_2_171_2","doi-asserted-by":"publisher","DOI":"10.1145\/3110272"},{"key":"e_1_3_2_172_2","doi-asserted-by":"publisher","DOI":"10.1145\/2854146"},{"key":"e_1_3_2_173_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00114"},{"key":"e_1_3_2_174_2","doi-asserted-by":"publisher","DOI":"10.1145\/3110261"},{"key":"e_1_3_2_175_2","unstructured":"Proven Liam. 2022. Linux 6.1: Rust to Hit Mainline Kernel. Retrieved October 2022 from https:\/\/www.theregister.com\/2022\/10\/05\/rust_kernel_pull_request_pulled\/"},{"key":"e_1_3_2_176_2","unstructured":"Md Rakib Hossain Misu Cristina V. Lopes Iris Ma and James Noble. 2024. Towards AI-assisted synthesis of verified Dafny methods. arXiv:2402.00247. Retrieved from https:\/\/arxiv.org\/abs\/2402.00247"},{"key":"e_1_3_2_177_2","first-page":"1465","volume-title":"Proceedings of the 28th USENIX Security Symposium (USENIX Security \u201919)","author":"Ramananandro Tahina","year":"2019","unstructured":"Tahina Ramananandro, Antoine Delignat-Lavaud, C\u00e9dric Fournet, Nikhil Swamy, Tej Chajed, Nadim Kobeissi, and Jonathan Protzenko. 2019. EverParse: Verified secure zero-copy parsers for authenticated message formats. In Proceedings of the 28th USENIX Security Symposium (USENIX Security \u201919). Nadia Heninger and Patrick Traynor (Eds.), USENIX Association, 1465\u20131482."},{"key":"e_1_3_2_178_2","doi-asserted-by":"crossref","unstructured":"Tahina Ramananandro Gabriel Ebner Guido Mart\u00ednez and Nikhil Swamy. 2025. Secure Parsing and Serializing with Separation Logic Applied to CBOR CDDL and COSE. Retrieved May 2025 from https:\/\/arxiv.org\/abs\/2505.17335","DOI":"10.1145\/3719027.3765120"},{"key":"e_1_3_2_179_2","unstructured":"Tahina Ramananandro Aseem Rastogi and Nikhil Swamy. 2021. EverParse: Hardening Critical Attack Surfaces with Formally Proven Message Parsers. Retrieved May 2021 from https:\/\/www.microsoft.com\/en-us\/research\/blog\/everparse-hardening-critical-attack-surfaces-with-formally-proven-message-parsers\/"},{"key":"e_1_3_2_180_2","unstructured":"Aseem Rastogi Guido Mart\u00ednez Aymeric Fromherz Tahina Ramananandro and Nikhil Swamy. 2020. Programming and Proving with Indexed Effects. Retrieved July 2020 from https:\/\/fstar-lang.org\/papers\/indexedeffects\/indexedeffects.pdf"},{"key":"e_1_3_2_181_2","doi-asserted-by":"publisher","DOI":"10.1145\/3689773"},{"key":"e_1_3_2_182_2","unstructured":"Z. Z. Ren Zhihong Shao Junxiao Song Huajian Xin Haocheng Wang Wanjia Zhao Liyue Zhang Zhe Fu Qihao Zhu Dejian Yang et al. 2025. DeepSeek-Prover-V2: Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition. arXiv:2504.21801. Retrieved from https:\/\/arxiv.org\/abs\/2504.21801"},{"key":"e_1_3_2_183_2","doi-asserted-by":"crossref","unstructured":"E. Rescorla. 2018. The transport layer security (TLS) protocol version 1.3. Retrieved from https:\/\/www.rfc-editor.org\/info\/rfc8446","DOI":"10.17487\/RFC8446"},{"key":"e_1_3_2_184_2","doi-asserted-by":"crossref","unstructured":"Eric Rescorla Kazuho Oku Nick Sullivan and Christopher A. Wood. 2025. TLS Encrypted Client Hello. RFC Editor. Retrieved from https:\/\/www.rfc-editor.org\/info\/rfc9849","DOI":"10.17487\/RFC9849"},{"key":"e_1_3_2_185_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_3_2_186_2","doi-asserted-by":"publisher","DOI":"10.5555\/AAI28546929"},{"key":"e_1_3_2_187_2","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373823"},{"key":"e_1_3_2_188_2","first-page":"1","volume-title":"Proceedings of the 38th European Conference on Object-Oriented Programming (ECOOP \u201924)","volume":"313","author":"Robinson Amos","year":"2024","unstructured":"Amos Robinson and Alex Potanin. 2024. Pipit on the post: Proving pre- and post-conditions of reactive systems. In Proceedings of the 38th European Conference on Object-Oriented Programming (ECOOP \u201924). Jonathan Aldrich and Guido Salvaneschi (Eds.), LIPIcs, Vol. 313, Schloss Dagstuhl\u2014Leibniz-Zentrum f\u00fcr Informatik, Article 34, 1\u201328."},{"key":"e_1_3_2_189_2","doi-asserted-by":"publisher","DOI":"10.1145\/3394450.3397466"},{"key":"e_1_3_2_190_2","doi-asserted-by":"crossref","unstructured":"Jim Schaad. 2022. CBOR Object Signing and Encryption (COSE): Structures and Process. RFC 9052. Retrieved from https:\/\/www.rfc-editor.org\/info\/rfc9052","DOI":"10.17487\/RFC9052"},{"key":"e_1_3_2_191_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-025-09721-0"},{"key":"e_1_3_2_192_2","doi-asserted-by":"publisher","DOI":"10.1145\/3434307"},{"key":"e_1_3_2_193_2","volume-title":"Proceedings of the USENIX Security Symposium","author":"Singh Pratap","year":"2025","unstructured":"Pratap Singh, Joshua Gancher, and Bryan Parno. 2025. OwlC: Compiling security protocols to verified, secure, high-performance libraries. In Proceedings of the USENIX Security Symposium."},{"key":"e_1_3_2_194_2","doi-asserted-by":"publisher","DOI":"10.1145\/3706056"},{"key":"e_1_3_2_195_2","first-page":"571","article-title":"Self-certification: Bootstrapping certified typecheckers in F \\({}^{\\star}\\)  with Coq","author":"Strub Pierre-Yves","year":"2012","unstructured":"Pierre-Yves Strub, Nikhil Swamy, C\u00e9dric Fournet, and Juan Chen. 2012. Self-certification: Bootstrapping certified typecheckers in F \\({}^{\\star}\\) with Coq. In Proceedings of the Symposium on Principles of Programming Languages (POPL). ACM, 571\u2013584.","journal-title":"Proceedings of the Symposium on Principles of Programming Languages (POPL)"},{"key":"e_1_3_2_196_2","unstructured":"Chuyue Sun Ying Sheng Oded Padon and Clark Barrett. 2023. Clover: Closed-loop verifiable code generation. arXiv:2310.17807. Retrieved from https:\/\/arxiv.org\/abs\/2310.17807"},{"key":"e_1_3_2_197_2","volume-title":"Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI)","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, et al. 2024. Anvil: Verifying liveness of cluster management controllers. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI)."},{"key":"e_1_3_2_198_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11957-6_28"},{"key":"e_1_3_2_199_2","doi-asserted-by":"publisher","DOI":"10.1145\/2034574.2034811"},{"key":"e_1_3_2_200_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2006.02.003"},{"key":"e_1_3_2_201_2","doi-asserted-by":"publisher","DOI":"10.1145\/2914770.2837655"},{"key":"e_1_3_2_202_2","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523708"},{"key":"e_1_3_2_203_2","doi-asserted-by":"publisher","DOI":"10.1145\/3409003"},{"key":"e_1_3_2_204_2","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2491978"},{"key":"e_1_3_2_205_2","first-page":"1091","volume-title":"Proceedings of the 30th USENIX Security Symposium (USENIX Security \u201921)","author":"Tao Zhe","year":"2021","unstructured":"Zhe Tao, Aseem Rastogi, Naman Gupta, Kapil Vaswani, and Aditya V. Thakur., August. 2021. DICE*: A formally verified implementation of DICE measured boot. In Proceedings of the 30th USENIX Security Symposium (USENIX Security \u201921). USENIX Association, 1091\u20131107."},{"key":"e_1_3_2_206_2","unstructured":"Amitayush Thakur Yeming Wen and Swarat Chaudhuri. 2023. A language-agent approach to formal theorem-proving. arXiv:2310.04353. Retrieved from https:\/\/arxiv.org\/abs\/2310.04353"},{"key":"e_1_3_2_207_2","doi-asserted-by":"publisher","DOI":"10.1109\/MSP.2016.125"},{"key":"e_1_3_2_208_2","unstructured":"Trusted Computing Group. 2023. DICE Protection Environment Version 1.0 Revision 0.6. Retrieved from https:\/\/trustedcomputinggroup.org\/wp-content\/uploads\/TCG-DICE-Protection-Environment-Specification_14february2023-1.pdf"},{"key":"e_1_3_2_209_2","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134076"},{"key":"e_1_3_2_210_2","volume-title":"Proceedings of the IEEE\/ACM International Conference on Software Engineering: Software Engineering in Practice (ICSE-SEIP)","author":"VanHattum Alexa","year":"2022","unstructured":"Alexa VanHattum, Daniel Schwartz-Narbonne, Nathan Chong, and Adrian Sampson. 2022. Verifying dynamic trait objects in Rust. In Proceedings of the IEEE\/ACM International Conference on Software Engineering: Software Engineering in Practice (ICSE-SEIP)."},{"key":"e_1_3_2_211_2","doi-asserted-by":"crossref","unstructured":"Niki Vazou and Michael Greenberg. 2022. How to safely use extensionality in Liquid Haskell. arXiv:2103.02177. Retrieved from https:\/\/arxiv.org\/abs\/2103.02177","DOI":"10.1145\/3554301"},{"key":"e_1_3_2_212_2","doi-asserted-by":"publisher","DOI":"10.1145\/3658644.3690183"},{"key":"e_1_3_2_213_2","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75283"},{"key":"e_1_3_2_214_2","first-page":"1217","volume-title":"Proceedings of the 32nd USENIX Security Symposium (USENIX Security 23)","author":"Wallez Th\u00e9ophile","year":"2023","unstructured":"Th\u00e9ophile Wallez, Jonathan Protzenko, Benjamin Beurdouche, and Karthikeyan Bhargavan. 2023. TreeSync: Authenticated group management for messaging layer security. In Proceedings of the 32nd USENIX Security Symposium (USENIX Security 23), 1217\u20131233."},{"key":"e_1_3_2_215_2","doi-asserted-by":"publisher","DOI":"10.1145\/3576915.3623201"},{"key":"e_1_3_2_216_2","doi-asserted-by":"crossref","unstructured":"Th\u00e9ophile Wallez Jonathan Protzenko and Karthikeyan Bhargavan. 2025. TreeKEM: A modular machine-checked symbolic security analysis of group key agreement in messaging layer security. IACR Cryptology ePrint Archive 410.","DOI":"10.1109\/SP61157.2025.00228"},{"key":"e_1_3_2_217_2","unstructured":"Haiming Wang Mert Unsal Xiaohan Lin Mantas Baksys Junqi Liu Marco Dos Santos Flood Sung Marina Vinyes Zhenzhe Ying Zekai Zhu et al. 2025. Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning. arXiv: 2504.11354. Retrieved from https:\/\/arxiv.org\/abs\/2504.11354"},{"key":"e_1_3_2_218_2","unstructured":"White House Office of the National Cyber Director. 2024. Back to the Building Blocks: A Path toward Secure and Measurable Software. Retrieved February 2024 from https:\/\/bidenwhitehouse.archives.gov\/wp-content\/uploads\/2024\/02\/Final-ONCD-Technical-Report.pdf"},{"key":"e_1_3_2_219_2","volume-title":"Proceedings of the 28th International Conference on Types for Proofs and Programs (TYPES)","author":"Winterhalter Th\u00e9o","year":"2022","unstructured":"Th\u00e9o Winterhalter, Cezar-Constantin Andrici, C\u0103t\u0103lin Hri\u0163cu, Kenji Maillard, Guido Mart\u00ednez, and Exequiel Rivas. 2022. Partial Dijkstra monads for all. In Proceedings of the 28th International Conference on Types for Proofs and Programs (TYPES)."},{"key":"e_1_3_2_220_2","doi-asserted-by":"publisher","DOI":"10.1145\/3485522"},{"key":"e_1_3_2_221_2","unstructured":"Jenny Xiang Daniel Schoepe and Marianna Rapoport. 2025. Transitioning production Software Verification to Verus: An Experience Report. Retrieved May 2025 from https:\/\/sites.google.com\/view\/rustverify2025"},{"key":"e_1_3_2_222_2","first-page":"6984","volume-title":"Proceedings of the International Conference on Machine Learning","author":"Yang Kaiyu","year":"2019","unstructured":"Kaiyu Yang and Jia Deng. 2019. Learning to prove theorems via interacting with proof assistants. In Proceedings of the International Conference on Machine Learning. PMLR, 6984\u20136994."},{"key":"e_1_3_2_223_2","volume-title":"Proceedings of the Advances in Neural Information Processing Systems","volume":"36","author":"Yang Kaiyu","year":"2024","unstructured":"Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan J. Prenger, and Animashree Anandkumar. 2024. LeanDojo: Theorem proving with retrieval-augmented language models. In Proceedings of the Advances in Neural Information Processing Systems, Vol. 36."},{"key":"e_1_3_2_224_2","volume-title":"Proceedings of the International Conference on Cryptographic Hardware and Embedded Systems (CHES)","author":"Yarom Yuval","year":"2010","unstructured":"Yuval Yarom, Daniel Genkin, and Nadia Heninger. 2010. CacheBleed: A timing attack on OpenSSL constant time RSA. In Proceedings of the International Conference on Cryptographic Hardware and Embedded Systems (CHES)."},{"key":"e_1_3_2_225_2","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3133974"},{"key":"e_1_3_2_226_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00101"},{"key":"e_1_3_2_227_2","volume-title":"Proceedings of the Formal Methods in Computer-Aided Design (FMCAD) Conference","author":"Zhou Yi","year":"2024","unstructured":"Yi Zhou, Jay Bosamiya, Jessica Li, Marijn Heule, and Bryan Parno. 2024. Context pruning for more robust SMT-based program verification. In Proceedings of the Formal Methods in Computer-Aided Design (FMCAD) Conference."},{"key":"e_1_3_2_228_2","volume-title":"Proceedings of the Formal Methods in Computer-Aided Design (FMCAD) Conference","author":"Zhou Yi","year":"2023","unstructured":"Yi Zhou, Jay Bosamiya, Yoshiki Takashima, Jessica Li, Marijn Heule, and Bryan Parno. 2023. Mariposa: Measuring SMT instability in automated program verification. In Proceedings of the Formal Methods in Computer-Aided Design (FMCAD) Conference."},{"key":"e_1_3_2_229_2","volume-title":"Proceedings of the ACM Conference on Computer and Communications Security (CCS)","author":"Zhou Yi","year":"2023","unstructured":"Yi Zhou, Sydney Gibson, Sarah Cai, Menucha Winchell, and Bryan Parno. 2023. Gal\u00e1pagos: Developing verified low-level cryptography on heterogeneous hardware. In Proceedings of the ACM Conference on Computer and Communications Security (CCS)."},{"key":"e_1_3_2_230_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-99984-0_5"},{"key":"e_1_3_2_231_2","volume-title":"Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Zhou Ziqiao","year":"2024","unstructured":"Ziqiao Zhou, Weiteng Chen, Chris Hawblitzel, and Weidong Cui. 2024. VeriSMo: A verified security module for confidential VMs. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI)."},{"key":"e_1_3_2_232_2","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134043"},{"key":"e_1_3_2_233_2","volume-title":"Proceedings of the ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI)","author":"Ayoun Sacha \u00c9lie","year":"2024","unstructured":"Sacha \u00c9lie Ayoun, Xavier Denis, Petar Maksimovi\u0107, and Philippa Gardner. 2024. A hybrid approach to semi-automated Rust verification. In Proceedings of the ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI). ACM."}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3805702","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,5]],"date-time":"2026-06-05T14:02:20Z","timestamp":1780668140000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3805702"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,6,5]]},"references-count":232,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2026,6,30]]}},"alternative-id":["10.1145\/3805702"],"URL":"https:\/\/doi.org\/10.1145\/3805702","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,6,5]]},"assertion":[{"value":"2025-06-17","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-11-17","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-06-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}