Kani is a model checker that compiles Rust proof harnesses from MIR to CBMC for bounded verification of safety properties and supports contracts to extend checks to unbounded correctness.
Geller, Niki Vazou, and Ranjit Jhala
4 Pith papers cite this work. Polarity classification is still indexing.
4
Pith papers citing it
years
2026 4verdicts
UNVERDICTED 4representative citing papers
A large open crowdsourced effort verifies substantial parts of the Rust standard library for memory safety properties by integrating complementary verification tools into CI on a forked repository.
LBAC is a new programming model that enforces user-specified policies on agentic applications by requiring agent-generated programs to be well-typed in the context of the scaffolding code.
Ranger is a bidirectional refinement type system for integer range types, implemented in the Licorne language, that integrates inference and flow analysis to verify bounds properties with low annotation overhead compared to Java, Scala, Checker Framework, and Liquid Java.
citing papers explorer
-
Kani: A Model Checker for Rust
Kani is a model checker that compiles Rust proof harnesses from MIR to CBMC for bounded verification of safety properties and supports contracts to extend checks to unbounded correctness.
-
Verifying the Rust Standard Library
A large open crowdsourced effort verifies substantial parts of the Rust standard library for memory safety properties by integrating complementary verification tools into CI on a forked repository.
-
Language-Based Agent Control
LBAC is a new programming model that enforces user-specified policies on agentic applications by requiring agent-generated programs to be well-typed in the context of the scaffolding code.
-
Practical Range Refinement Types with Inference
Ranger is a bidirectional refinement type system for integer range types, implemented in the Licorne language, that integrates inference and flow analysis to verify bounds properties with low annotation overhead compared to Java, Scala, Checker Framework, and Liquid Java.