Kani es un verificador de modelos de código abierto diseñado para el lenguaje de programación Rust. El artículo, publicado en arXiv en julio de 2026, lo presenta como una herramienta que lleva la verificación acotada más allá de la búsqueda de errores y ofrece garantías formales de corrección. Aunque el sistema de tipos por propiedad (ownership) de Rust evita en buena medida errores de memoria en código seguro, sigue habiendo propiedades que el compilador no garantiza: la corrección de operaciones inseguras —como la desreferencia de punteros crudos—, la corrección funcional de los algoritmos y la ausencia de pánicos en tiempo de ejecución. Kani aborda estas cuestiones compilando arneses de prueba desde la representación intermedia de nivel medio de Rust (MIR) hacia el motor de verificación bit-a-bit de CBMC, comprobando de forma automática un conjunto amplio de propiedades de seguridad sin anotaciones por parte del usuario.
Para extender la verificación del ámbito acotado al no acotado, la herramienta incorpora un lenguaje de especificación con contratos de funciones, contratos de bucles, cuantificadores y stubs de funciones. Los autores ilustran su utilidad con estudios de caso en proyectos industriales de Rust, donde los contratos llevaron la verificación desde la mera ausencia de pánicos hasta la demostración de corrección funcional y permitieron descubrir seis defectos hasta entonces desconocidos. Kani se ejecuta a escala en pipelines de integración continua: en la campaña de verificación de la biblioteca estándar de Rust procesa más de 16.000 arneses por cada cambio de código.