Kani: el verificador de modelos que garantiza la corrección del código Rust en producción

Kani: A Model Checker for Rust

El sistema de tipos de Rust previene errores de memoria en código seguro, pero no garantiza la solidez de las operaciones unsafe, la corrección funcional ni la ausencia de panics. Kani, un verificador de modelos de código abierto, compila harnesses de prueba desde la representación intermedia de Rust (MIR) hacia el motor de verificación bit-precisa de CBMC, comprobando automáticamente un amplio conjunto de propiedades de seguridad sin anotaciones del usuario. Para ampliar la verificación de acotada a no acotada, Kani ofrece un lenguaje de especificación con contratos de funciones y bucles, cuantificadores y stubbing. En casos de estudio con proyectos industriales, los contratos elevaron la verificación de la ausencia de panics a la corrección funcional, descubriendo seis errores desconocidos. Kani opera a escala en CI de producción, con más de 16,000 harnesses verificados por cambio de código en la campaña de verificación de la biblioteca estándar de Rust.