pith. sign in

arxiv: 2607.01504 · v1 · pith:NCJM7G3Dnew · submitted 2026-07-01 · 💻 cs.SE · cs.LO· cs.PL

Kani: A Model Checker for Rust

R\'emi Delmas , Zyad Hassan , Qinheping Hu , Rahul Kumar , Felipe R. Monteiro , Thanh Nguyen , Adri\'an Palacios , Celina Val
show 4 more authors
Michael Tautschnig Justus Adam Daniel Schwartz-Narbonne Carolyn Zech
This is my paper

Pith reviewed 2026-07-03 18:59 UTC · model grok-4.3

classification 💻 cs.SE cs.LOcs.PL
keywords model checkingRustverificationMIRCBMCunsafe codecontractspanic freedom
0
0 comments X

The pith

Kani translates Rust MIR into CBMC to verify soundness of unsafe code, functional correctness, and panic freedom.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

Kani is a model checker that compiles Rust's mid-level intermediate representation directly into the CBMC bounded model checker. It automatically checks a broad set of safety properties on proof harnesses without requiring manual annotations. To handle unbounded properties, the tool adds a specification language with function contracts, loop contracts, quantifiers, and stubbing. The approach has been deployed at scale, running over 16,000 harnesses on every change to the Rust standard library. This shifts verification from bug detection toward providing guarantees on properties that Rust's type system does not address.

Core claim

Kani compiles proof harnesses from Rust's Mid-level Intermediate Representation (MIR) into CBMC's bit-precise verification engine, automatically checking a comprehensive set of safety properties with no user annotation. To extend verification from bounded to unbounded, Kani provides a specification language comprising function contracts, loop contracts, quantifiers, and function stubbing. Case studies on industrial Rust projects show contracts upgrading verification from panic-freedom to functional correctness and uncovering previously unknown bugs.

What carries the argument

Compilation step that maps Rust MIR programs and harnesses into CBMC's bit-precise input language while preserving semantics for the checked properties.

Load-bearing premise

The mapping from Rust MIR to CBMC's model preserves the original program's observable behavior for the properties being checked.

What would settle it

A concrete Rust program containing an unsafe operation that triggers a runtime error or violates a stated contract, yet Kani reports the harness as verified.

Figures

Figures reproduced from arXiv: 2607.01504 by Adri\'an Palacios, Carolyn Zech, Celina Val, Daniel Schwartz-Narbonne, Felipe R. Monteiro, Justus Adam, Michael Tautschnig, Qinheping Hu, Rahul Kumar, R\'emi Delmas, Thanh Nguyen, Zyad Hassan.

Figure 1
Figure 1. Figure 1: Kani verification pipeline. Blue boxes are Kani components; gray boxes are external tools; green is the orchestrator. [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
read the original abstract

Rust's ownership type system prevents memory errors in safe code, but certain desirable properties remain orthogonal to compilation: the soundness of unsafe operations (e.g., raw pointer dereferences), functional correctness, and absence of runtime panics. We present Kani, an open-source model checker for Rust that pushes bounded model checking beyond bug-finding to provide correctness guarantees for these properties. Kani compiles proof harnesses from Rust's Mid-level Intermediate Representation (MIR) into CBMC's bit-precise verification engine, automatically checking a comprehensive set of safety properties with no user annotation. To extend verification from bounded to unbounded, Kani provides a specification language comprising function contracts, loop contracts, quantifiers, and function stubbing. We demonstrate feasibility through case studies on industrial Rust projects, where contracts upgraded verification from panic-freedom to functional correctness, uncovering six previously unknown bugs. Kani operates at scale in production CI, with over 16,000 harnesses verified per code change in the Rust standard library verification campaign.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 1 minor

Summary. The paper presents Kani, an open-source bounded model checker for Rust. It compiles proof harnesses from Rust's MIR into CBMC's bit-precise engine to automatically check safety properties (soundness of unsafe operations, functional correctness, absence of panics) with no user annotation. A specification language with function/loop contracts, quantifiers, and stubbing extends verification to unbounded cases. Feasibility is shown via case studies on industrial projects (contracts upgraded verification and found six bugs) and a production CI campaign verifying over 16,000 harnesses per change in the Rust standard library.

Significance. If the MIR-to-CBMC translation is semantics-preserving, Kani supplies a scalable, annotation-light tool that moves Rust verification from bug-finding to correctness guarantees, particularly for unsafe code. The scale of the std-lib campaign and the contract-based upgrade from panic-freedom to functional correctness are concrete strengths; the open-source release and CI integration further increase practical impact.

major comments (2)
  1. [Abstract] Abstract (compilation paragraph) and the description of the MIR-to-CBMC step: the central claim that Kani 'provides correctness guarantees' for unsafe operations, functional correctness, and panic freedom rests on the unstated assumption that the translation from Rust MIR to the CBMC model preserves semantics exactly (including raw pointers, panics, and ownership). No proof sketch, equivalence argument, testing suite, or soundness discussion is supplied; this is load-bearing for every guarantee asserted in the paper.
  2. [Specification language section (implied by abstract)] The contract semantics and their interaction with the bounded engine are described at a high level but receive no formal treatment or soundness argument. Because contracts are the mechanism that 'extends verification from bounded to unbounded,' the absence of any discussion of their soundness (or of error bounds on the resulting claims) directly weakens the functional-correctness results reported in the case studies.
minor comments (1)
  1. [Abstract] The abstract states 'over 16,000 harnesses verified per code change' but supplies no table, section, or breakdown showing how many harnesses target unsafe code versus safe code, or how many use contracts versus pure bounded checking.

Simulated Author's Rebuttal

2 responses · 1 unresolved

We thank the referee for the detailed and constructive report. We address the two major comments below, clarifying the scope of the current manuscript and what can be strengthened in revision.

read point-by-point responses

  1. Referee: [Abstract] Abstract (compilation paragraph) and the description of the MIR-to-CBMC step: the central claim that Kani 'provides correctness guarantees' for unsafe operations, functional correctness, and panic freedom rests on the unstated assumption that the translation from Rust MIR to the CBMC model preserves semantics exactly (including raw pointers, panics, and ownership). No proof sketch, equivalence argument, testing suite, or soundness discussion is supplied; this is load-bearing for every guarantee asserted in the paper.

    Authors: We agree that the manuscript does not supply a formal proof sketch or equivalence argument establishing that the MIR-to-CBMC translation is semantics-preserving. The implementation maps MIR constructs (including raw pointers, panics, and ownership) to CBMC's bit-precise C model, and correctness is supported by the extensive case studies and the production-scale verification of the Rust standard library. A complete formal argument would require mechanized semantics for both MIR and CBMC and lies outside the scope of this tool paper. We will add an explicit subsection in the revised version that states the translation assumptions, known limitations, and the validation performed via testing and industrial use. revision: partial

  2. Referee: [Specification language section (implied by abstract)] The contract semantics and their interaction with the bounded engine are described at a high level but receive no formal treatment or soundness argument. Because contracts are the mechanism that 'extends verification from bounded to unbounded,' the absence of any discussion of their soundness (or of error bounds on the resulting claims) directly weakens the functional-correctness results reported in the case studies.

    Authors: We acknowledge that the contract semantics receive only a high-level description and that no formal soundness argument or error-bound analysis is provided. Contracts are encoded as assumptions and assertions inside the bounded CBMC engine, with stubbing and quantifiers handled via CBMC's support for them; this allows the reported upgrade from panic-freedom to functional correctness in the case studies. A full formal treatment would constitute a separate contribution. In revision we will expand the specification-language section to include the concrete encoding strategy, the over-approximations introduced, and the practical validation obtained from the industrial examples. revision: partial

standing simulated objections not resolved
  • A complete formal proof of semantics preservation for the MIR-to-CBMC translation and a formal soundness argument for the contract semantics.

Circularity Check

0 steps flagged

No circularity: tool-description paper with no derivation chain or self-referential equations

full rationale

The paper is a description of an implemented model checker (Kani) that translates Rust MIR to CBMC. No equations, fitted parameters, uniqueness theorems, or ansatzes appear in the provided text. The central claim rests on the engineering assumption that the MIR-to-CBMC translation preserves semantics, but this assumption is not derived from or reduced to any prior result within the paper itself; it is simply stated as the basis of the implementation. No self-citation load-bearing steps, self-definitional constructs, or renamed known results are present. The work is therefore self-contained as an empirical tool report rather than a closed mathematical derivation.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The central claim rests on the unproven assumption that the MIR-to-CBMC translation is semantics-preserving and that user-written contracts are correctly interpreted by the checker.

axioms (2)
  • domain assumption MIR-to-CBMC translation preserves the observable behavior of the original Rust program.
    Invoked in the compilation step described in the abstract; if false, verification results do not transfer to Rust source.
  • domain assumption User-provided contracts and loop invariants are semantically faithful to the intended specification.
    Required for the upgrade from panic-freedom to functional correctness claims.

pith-pipeline@v0.9.1-grok · 5746 in / 1261 out tokens · 22523 ms · 2026-07-03T18:59:15.156060+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

46 extracted references · 29 canonical work pages

  1. [1]

    Alexandru Agache, Marc Brooker, Alexandra Iordache, Anthony Liguori, Rolf Neugebauer, Phil Piwonka, and Diana-Maria Popa. 2020. Firecracker: Light- weight Virtualization for Serverless Applications. In17th USENIX Symposium on Networked Systems Design and Implementation (NSDI). USENIX Association, Santa Clara, CA, USA, 419–434

    2020

  2. [2]

    Amazon Web Services. 2024. s2n-quic: An implementation of the IETF QUIC protocol. https://github.com/aws/s2n-quic

    2024

  3. [3]

    Apt, Frank S

    Krzysztof R. Apt, Frank S. de Boer, and Ernst-Rüdiger Olderog. 2009.Verification of Sequential and Concurrent Programs(3rd ed.). Springer, Berlin, Heidelberg. doi:10.1007/978-1-84882-745-5

    work page doi:10.1007/978-1-84882-745-5 2009

  4. [4]

    Vytautas Astrauskas, Aurel Bílý, Jonáš Fiala, Zachary Grannan, Christoph Matheja, Peter Müller, Federico Poli, and Alexander J. Summers. 2022. The Prusti Project: Formal Verification for Rust. InNASA Formal Methods: 14th In- ternational Symposium, NFM 2022, Pasadena, CA, USA, May 24–27, 2022, Pro- ceedings(Pasadena, CA, USA). Springer-Verlag, Berlin, Heid...

    work page doi:10.1007/978-3-031-06773-0_5 2022

  5. [5]

    Vytautas Astrauskas, Christoph Matheja, Federico Poli, Peter Müller, and Alexan- der J. Summers. 2020. How Do Programmers Use Unsafe Rust?Proc. ACM Program. Lang.4, OOPSLA, Article 136 (2020), 27 pages. doi:10.1145/3428204

    work page doi:10.1145/3428204 2020

  6. [6]

    Yechan Bae, Youngsuk Kim, Ammar Askar, Jungwon Lim, and Taesoo Kim. 2021. Rudra: Finding Memory Safety Bugs in Rust at the Ecosystem Scale. InProc. ACM SIGOPS 28th Symposium on Operating Systems Principles (SOSP). Association for Computing Machinery, New York, NY, USA, 84–99. doi:10.1145/3477132.3483570

    work page doi:10.1145/3477132.3483570 2021

  7. [7]

    Haniel Barbosa, Clark Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, and Yoni Zohar. 2022. cvc5: A Versatile and Industrial-Strength SMT Solver. InTools and Algorithms for the Construction and An...

    work page doi:10.1007/978-3-030-99524-9_24 2022

  8. [8]

    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. InVerified Software. Theories, Tools and Experiments (VSTTE). Springer, Cham, 96–119. doi:10.1007/978-3-031-86695-1_7

    work page doi:10.1007/978-3-031-86695-1_7 2025

  9. [9]

    Karthikeyan Bhargavan, Lasse Letager Hansen, Franziskus Kiefer, Jonas Schneider-Bensch, and Bas Spitters. 2025. Formal Security and Functional Verifi- cation of Cryptographic Protocol Implementations in Rust. InProceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security(Taipei, Taiwan)(CCS ’25). Association for Computing Machiner...

    work page doi:10.1145/3719027.3765213 2025

  10. [10]

    Armin Biere, Alessandro Cimatti, Edmund Clarke, and Yunshan Zhu. 1999. Sym- bolic Model Checking without BDDs. InTools and Algorithms for the Construction and Analysis of Systems (TACAS) (Lecture Notes in Computer Science, Vol. 1579). Springer, Berlin, Heidelberg, 193–207. doi:10.1007/3-540-49059-0_14

    work page doi:10.1007/3-540-49059-0_14 1999

  11. [11]

    Armin Biere, Katalin Fazekas, Mathias Fleury, and Maximillian Heisinger. 2020. CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling Entering the SAT Compe- tition 2020. InProc. of SAT Competition 2020 – Solver and Benchmark Descriptions (Department of Computer Science Report Series B, Vol. B-2020-1), Tomas Balyo, Nils Froleyks, Marijn Heule, Markus Iser...

    2020

  12. [12]

    Kevin Boos, Namitha Liyanage, Ramla Ijaz, and Lin Zhong. 2020. Theseus: an experiment in operating system structure and state management. InProceedings of the 14th USENIX Conference on Operating Systems Design and Implementation (OSDI’20). USENIX Association, USA, Article 1, 19 pages

    2020

  13. [13]

    Monteiro, Daniel Schwartz-Narbonne, Ser- dar Tasiran, Michael Tautschnig, and Mark R

    Nathan Chong, Byron Cook, Jonathan Eidelman, Konstantinos Kallas, Kareem Khazem, Felipe R. Monteiro, Daniel Schwartz-Narbonne, Ser- dar Tasiran, Michael Tautschnig, and Mark R. Tuttle. 2021. Code- level model checking in the software development workflow at Amazon Web Services.Software: Practice and Experience51, 4 (2021), 772–797. arXiv:https://onlinelib...

    work page doi:10.1002/spe.2949 2021

  14. [14]

    Monteiro, Daniel Schwartz-Narbonne, Serdar Tasiran, Michael Tautschnig, and Mark R

    Nathan Chong, Byron Cook, Konstantinos Kallas, Kareem Khazem, Felipe R. Monteiro, Daniel Schwartz-Narbonne, Serdar Tasiran, Michael Tautschnig, and Mark R. Tuttle. 2020. Code-level model checking in the software development workflow. InProceedings of the ACM/IEEE 42nd International Conference on Soft- ware Engineering: Software Engineering in Practice(Seo...

    work page doi:10.1145/3377813.3381347 2020

  15. [15]

    Andrey Chudnov, Nathan Collins, Byron Cook, Joey Dodds, Brian Huffman, Colm MacCárthaigh, Stephen Magill, Eric Mertens, Eric Mullen, Serdar Tasiran, Aaron Tomb, and Eddy Westbrook. 2018. Continuous Formal Verification of Amazon s2n. InComputer Aided Verification (CA V) (Lecture Notes in Computer Science, Vol. 10982). Springer, Cham, 430–446. doi:10.1007/9...

    work page doi:10.1007/978-3-319-96142-2_26 2018

  16. [16]

    Edmund Clarke, Daniel Kroening, and Flavio Lerda. 2004. A Tool for Checking ANSI-C Programs. InTools and Algorithms for the Construction and Analysis of Systems (TACAS) (LNCS, Vol. 2988). Springer, Berlin, Heidelberg, 168–176. doi:10.1007/978-3-540-24730-2_15

    work page doi:10.1007/978-3-540-24730-2_15 2004

  17. [17]

    Monteiro, Thanh Nguyen, Rebecca Rumbul, Michael Tautschnig, Celina Val, and Carolyn Zech

    Byron Cook, Remi Delmas, Zyad Hassan, Bart Jacobs, Ranjit Jhala, Rahul Kumar, Felipe R. Monteiro, Thanh Nguyen, Rebecca Rumbul, Michael Tautschnig, Celina Val, and Carolyn Zech. 2026. Verifying the Rust Standard Library. InNASA Formal Methods (NFM). Springer, Cham, 1–20. To appear

    2026

  18. [18]

    Mohan Cui, Shuran Sun, Hui Xu, and Yangfan Zhou. 2024. Is Unsafe an Achilles’ Heel? A Comprehensive Study of Safety Requirements in Unsafe Rust Program- ming. InProc. IEEE/ACM 46th International Conference on Software Engineering (ICSE). Association for Computing Machinery, New York, NY, USA, 13 pages. doi:10.1145/3597503.3639136

    work page doi:10.1145/3597503.3639136 2024

  19. [19]

    Joseph W. Cutler, Craig Disselkoen, Aaron Eline, Shaobo He, Kyle Headley, Michael Hicks, Kesha Hietala, Eleftherios Ioannidis, John Kastner, Anwar Mamat, Darin McAdams, Matt McCutchen, Neha Rungta, Emina Torlak, and Andrew M. Wells. 2024. Cedar: A New Language for Expressive, Fast, Safe, and Analyz- able Authorization.Proc. ACM Program. Lang.8, OOPSLA1, A...

    work page doi:10.1145/3649835 2024

  20. [20]

    Datadog. 2024. lading: A load-testing framework. https://github.com/DataDog/ lading

    2024

  21. [21]

    Leonardo de Moura and Nikolaj Bjørner. 2008. Z3: An Efficient SMT Solver. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS) (LNCS, Vol. 4963). Springer, Berlin, Heidelberg, 337–340. doi:10.1007/978-3-540-78800- 3_24

    work page doi:10.1007/978-3-540-78800- 2008

  22. [22]

    Xavier Denis, Jacques-Henri Jourdan, and Claude Marché. 2022. Creusot: A Foundry for the Deductive Verification of Rust Programs. InFormal Methods and Software Engineering (ICFEM) (LNCS, Vol. 13478). Springer, Cham, 90–105. doi:10.1007/978-3-031-17244-1_6

    work page doi:10.1007/978-3-031-17244-1_6 2022

  23. [23]

    Niklas Eén and Niklas Sörensson. 2003. An Extensible SAT-solver. InTheory and Applications of Satisfiability Testing (SAT) (LNCS, Vol. 2919). Springer, Berlin, Heidelberg, 502–518. doi:10.1007/978-3-540-24605-3_37

    work page doi:10.1007/978-3-540-24605-3_37 2003

  24. [24]

    Lennard Gäher, Michael Sammler, Ralf Jung, Robbert Krebbers, and Derek Dreyer

  25. [25]

    ACM Program

    RefinedRust: A Type System for High-Assurance Verification of Rust Programs.Proc. ACM Program. Lang.8, PLDI, Article 192 (2024), 26 pages. doi:10. 1145/3656422

    2024

  26. [26]

    Son Ho and Jonathan Protzenko. 2022. Aeneas: Rust Verification by Functional Translation.Proc. ACM Program. Lang.6, ICFP (2022), 711–741. doi:10.1145/ 3547647

    2022

  27. [27]

    Li Huang, Sophie Ebersold, Alexander Kogtenkov, Bertrand Meyer, and Yinling Liu. 2026. Lessons from Formally Verified Deployed Software Systems.ACM Comput. Surv.58, 8, Article 212 (Feb. 2026), 37 pages. doi:10.1145/3785652

    work page doi:10.1145/3785652 2026

  28. [28]

    Bart Jacobs, Jan Smans, Pieter Philippaerts, Frédéric Vogels, Willem Penninckx, and Frank Piessens. 2011. VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java. InNASA Formal Methods (NFM) (Lecture Notes in Computer Science, Vol. 6617). Springer, Berlin, Heidelberg, 41–55. doi:10.1007/978-3-642-20398-5_4

    work page doi:10.1007/978-3-642-20398-5_4 2011

  29. [29]

    Ralf Jung, Hoang-Hai Dang, Jeehoon Kang, and Derek Dreyer. 2019. Stacked borrows: an aliasing model for Rust.Proc. ACM Program. Lang.4, POPL, Article 41 (Dec. 2019), 32 pages. doi:10.1145/3371109

    work page doi:10.1145/3371109 2019

  30. [30]

    Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer. 2017. RustBelt: securing the foundations of the Rust programming language.Proc. ACM Program. Lang.2, POPL, Article 66 (Dec. 2017), 34 pages. doi:10.1145/3158154

    work page doi:10.1145/3158154 2017

  31. [31]

    Ralf Jung, Benjamin Kimock, Christian Poveda, Eduardo Sánchez Muñoz, Oli Scherer, and Qian Wang. 2026. Miri: Practical Undefined Behavior Detection for Rust.Proc. ACM Program. Lang.10, POPL, Article 48 (2026), 31 pages. doi:10. 1145/3776690

    2026

  32. [32]

    Daniel Kroening, Peter Schrammel, and Michael Tautschnig. 2023. CBMC: The C Bounded Model Checker. arXiv:2302.02384

    work page arXiv 2023

  33. [33]

    Daniel Kroening and Michael Tautschnig. 2014. CBMC – C Bounded Model Checker. InTools and Algorithms for the Construction and Analysis of Systems, Erika Ábrahám and Klaus Havelund (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 389–391. https://doi.org/10.1007/978-3-642-54862-8_26

    work page doi:10.1007/978-3-642-54862-8_26 2014

  34. [34]

    Adam Langley, Alistair Riddoch, Alyssa Wilk, Antonio Vicente, Charles Krasic, Dan Zhang, Fan Yang, Fedor Kouranov, Ian Swett, Janardhan Iyengar, Jeff Bai- ley, Jeremy Dorfman, Jim Roskind, Joanna Kulik, Patrik Westin, Raman Tenneti, Robbie Shade, Ryan Hamilton, Victor Vasiliev, Wan-Teh Chang, and Zhongyi Shi

  35. [35]

    In Proceedings of the Conference of the ACM Special Interest Group on Data Commu- nication (SIGCOMM ’17)

    The QUIC Transport Protocol: Design and Internet-Scale Deployment. In Proceedings of the Conference of the ACM Special Interest Group on Data Commu- nication (SIGCOMM ’17). Association for Computing Machinery, New York, NY, USA, 183–196. doi:10.1145/3098822.3098842

    work page doi:10.1145/3098822.3098842

  36. [36]

    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.Proc. ACM Program. Lang.7, OOPSLA2, Article 286 (2023), 32 pages. doi:10.1145/3586037

    work page doi:10.1145/3586037 2023

  37. [37]

    Geller, Niki Vazou, and Ranjit Jhala

    Nico Lehmann, Adam T. Geller, Niki Vazou, and Ranjit Jhala. 2023. Flux: Liquid Types for Rust.Proc. ACM Program. Lang.7, PLDI, Article 169 (June 2023), 25 pages. doi:10.1145/3591283

    work page doi:10.1145/3591283 2023

  38. [38]

    Giffin, Pat Pannuto, Prabal Dutta, and Philip Levis

    Amit Levy, Bradford Campbell, Branden Ghena, Daniel B. Giffin, Pat Pannuto, Prabal Dutta, and Philip Levis. 2017. Multiprogramming a 64kB Computer Safely and Efficiently. InProceedings of the 26th Symposium on Operating Systems ASE ’26, October 12–16, 2026, Munich, Germany Delmas et al. Principles(Shanghai, China)(SOSP ’17). Association for Computing Mach...

    work page doi:10.1145/3132747.3132786 2017

  39. [39]

    Joshua Liebow-Feeser and Jack Wrenn. 2024. zerocopy: Zero-cost memory manipulation. https://github.com/google/zerocopy

    2024

  40. [40]

    Aina Niemetz and Mathias Preiner. 2023. Bitwuzla. InComputer Aided Verification (CA V) (LNCS, Vol. 13965). Springer, Cham, 3–17. doi:10.1007/978-3-031-37703-7_1

    work page doi:10.1007/978-3-031-37703-7_1 2023

  41. [41]

    OASIS. 2019. Virtual I/O Device (VIRTIO) Version 1.1. https://docs.oasis-open. org/virtio/virtio/v1.1/virtio-v1.1.html

    2019

  42. [42]

    Christopher Rabotin. 2024. Hifitime: A High-Fidelity Time Management Library. https://nyxspace.com/hifitime/

    2024

  43. [43]

    rust-osdev contributors. 2024. x86_64: Library for x86_64 specific functionality. https://github.com/rust-osdev/x86_64

    2024

  44. [44]

    seL4 Foundation. 2024. rust-sel4: Rust bindings for the seL4 microkernel. https: //github.com/seL4/rust-sel4

    2024

  45. [45]

    Alexa VanHattum, Daniel Schwartz-Narbonne, Nathan Chong, and Adrian Samp- son. 2022. Verifying dynamic trait objects in Rust. InProceedings of the 44th International Conference on Software Engineering: Software Engineering in Prac- tice (ICSE-SEIP ’22). Association for Computing Machinery, New York, NY, USA, 321–330. doi:10.1145/3510457.3513031

    work page doi:10.1145/3510457.3513031 2022

  46. [46]

    Neven Villani, Johannes Hostert, Derek Dreyer, and Ralf Jung. 2025. Tree Borrows. Proc. ACM Program. Lang.9, PLDI, Article 188 (2025), 28 pages. doi:10.1145/ 3735592

    2025