Research

Publications about Kani

• Rémi Delmas, Zyad Hassan, Qinheping Hu, Rahul Kumar, Felipe R. Monteiro, Thanh Nguyen, Adrián Palacios, Celina Val, Michael Tautschnig, Justus Adam, Daniel Schwartz-Narbonne, and Carolyn Zech. 2026. Kani: A Model Checker for Rust. Proceedings of the 41st IEEE/ACM International Conference on Automated Software Engineering (ASE '26), Munich, Germany, October 12-16, 2026.
• Alexa VanHattum, Daniel Schwartz-Narbonne, Nathan Chong, and Adrian Sampson. 2022. Verifying Dynamic Trait Objects in Rust. Proceedings of the 44th International Conference on Software Engineering: Software Engineering in Practice (ICSE-SEIP '22), May 2022, pp. 321-330. Video of the presentation.

Publications using Kani

This is not an exhaustive list.

• Minghua Wang, Yuxi Ling, Mingzhi Gao, Yuwei Liu, and Lin Huang. 2026. KaPilot: LLM-Assisted Generation of Kani Specifications for Unsafe Rust Verification. arXiv:2607.21957. LLM agents generate Kani specifications for unsafe Rust functions.
• Minghua Wang, Yuwei Liu, and Lin Huang. 2026. HarnessLLM: Rust Verification Harness Generation with Large Language Models. Proceedings of the 48th IEEE/ACM International Conference on Software Engineering (ICSE '26), pp. 742-753. LLM-generated Rust harnesses that are compiled and checked with Kani.
• Seth Dobrin and Łukasz Chmiel. 2026. The Unfireable Safety Kernel: Execution-Time AI Alignment for AI Agents and Other Escapable AI Systems. arXiv:2606.26057. Kani proves properties of a production Rust decision function.
• Nathaniel Macasaet. 2026. Emmy: The Search for Distributed Robustness through Algebraic Properties via Fuzz Testing and Bounded Model Checking. Technical Report UCB/EECS-2026-132, University of California, Berkeley, May 2026. Combines fuzzing with Kani to check algebraic properties.
• 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. NASA Formal Methods (NFM 2026), LNCS vol. 16622, pp. 415-435.
• Ian McCormack, Tomás Dougan, Sam Estep, Hanan Hibshi, Jonathan Aldrich, and Joshua Sunshine. 2026. A Mixed Methods Study on the Implications of Unsafe Rust for Interoperation, Encapsulation, and Tooling. ACM Transactions on Software Engineering and Methodology (TOSEM). Interviews and a survey of Rust developers, some of whom use Kani.
• Youcheng Sun, Jiawen Liu, Daniel Kroening, and Jason Xue. 2026. Agentic Model Checking. arXiv:2605.21434. LLM agents with bounded model checking back ends; Kani is the Rust back end.
• Sacha-Élie Ayoun, Opale Sjöstedt, and Azalea Raad. 2025. Soteria: Efficient Symbolic Execution as a Functional Library. arXiv:2511.08729. Uses Kani as a baseline in its evaluation.
• Alex Le Blanc and Patrick Lam. 2025. Lessons Learned So Far From a Community Effort to Verify the Rust Standard Library (work-in-progress). arXiv:2510.01072.
• Aidan Z.H. Yang, Yoshiki Takashima, Brandon Paulsen, Josiah Dodds, and Daniel Kroening. 2025. VERT: Polyglot Verified Equivalent Rust Transpilation with Large Language Models. 40th IEEE/ACM International Conference on Automated Software Engineering (ASE 2025), pp. 1453-1463. Checks LLM translations to Rust for equivalence using Bolero with Kani.
• Pei-Wei Chen, Shaokai Lin, Adwait Godbole, Ramneet Singh, Elizabeth Polgreen, Edward A. Lee, and Sanjit A. Seshia. 2025. PolyVer: A Compositional Approach for Polyglot System Modeling and Verification. arXiv:2503.03207. Kani verifies the Rust components of polyglot systems.
• Alex Le Blanc and Patrick Lam. 2024. Surveying the Rust Verification Landscape. arXiv:2410.01981.
• Yoshiki Takashima. 2023. PropProof: Free Model-Checking Harnesses from PBT. Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE '23), pp. 1903-1913. Turns Rust property-based tests into Kani harnesses.
• OtterSec. 2023. Solana formal verification: a case study. OtterSec blog. Industry blog post that discusses Kani.

To cite Kani, see the citation instructions in the repository README.