Puedes probar que tu código Rust es correcto sin escribir una sola prueba, pero el espacio de estados es la factura

Puedes probar que tu código Rust es correcto sin escribir una sola prueba. La herramienta que lo hace se llama model checker, y para Rust el más práctico en este momento es Kani, construido por AWS. Escribes assertions normales de Rust. Kani las convierte en claims matemáticos y las verifica para cada entrada posible. Sin theorem provers. Sin proof assistants. Sin desviaciones de seis meses hacia Coq.

El problema es que “cada entrada posible” solo funciona cuando el espacio de entrada es lo suficientemente pequeño para agotarlo. Si tu función recibe un Vec<u8> con un millón de elementos, Kani no verificará cada permutación. Verificará hasta un límite que especifiques, o correrá hasta que tu laptop se quede sin RAM. La prueba es real, pero está acotada.

Qué significa realmente “prueba sin pruebas”

La verificación formal suele significar escribir tu programa en un proof assistant como Coq, definir invariantes a mano y guiar al solver a través de pasos tácticos. Un compiler verificado como CompCert tomó años. La mayoría de los equipos no tienen años.

El model checking es diferente. Escribes Rust normal. Agregas una función de test anotada con #[kani::proof]. Dentro, creas valores simbólicos con kani::any(), llamas a tu código y haces assertions. Kani compila tu código a una fórmula lógica y se la entrega a un SMT solver. El solver confirma que la propiedad se cumple para todas las entradas dentro del límite, o produce un contraejemplo concreto.

No escribiste una prueba. Escribiste un test con un cuantificador universal. La herramienta escribió la prueba.

Cómo Kani convierte Rust en lógica

Kani es un bounded model checker. Desenrolla tu código en una fórmula lógica y le pregunta a un SMT solver si algún camino de ejecución puede violar una assertion. El solver trata las variables como simbólicas. Un test normal le da a x el valor 5. Una prueba de Kani le da a x un símbolo que representa cada u32 posible.

Aquí hay un ejemplo trivial. Tenemos una función que nunca debería desbordarse, y queremos probarlo.

// src/lib.rs
pub fn saturating_double(x: u32) -> u32 {
    x.saturating_mul(2)
}

#[cfg(kani)]
mod proofs {
    use super::*;

    #[kani::proof]
    fn check_saturating_double_never_overflows() {
        let x: u32 = kani::any();
        let result = saturating_double(x);
        if x > u32::MAX / 2 {
            assert_eq!(result, u32::MAX);
        } else {
            assert_eq!(result, x * 2);
        }
    }
}

Ejecuta cargo kani y Kani verifica esto en segundos. Revisa los 4.294.967.296 valores posibles de x sin ejecutarlos uno por uno. El SMT solver razona sobre la representación simbólica y concluye que no existe ningún contraejemplo.

El guard #[cfg(kani)] significa que este código solo se compila bajo Kani. No infla tu release build.

Un ejemplo real: probar que un parser nunca hace crash

Los desbordamientos son fáciles. Los casos interesantes dependen de los datos. Digamos que tenemos una función que parsea un pequeño header de protocol. Queremos probar que nunca hace panic, sin importar qué bytes le pasemos.

// src/protocol.rs
#[derive(Debug, PartialEq)]
pub enum ParseError {
    TooShort,
    InvalidVersion,
}

pub struct Header {
    pub version: u8,
    pub length: u16,
}

/// Parse a 4-byte header:
/// - byte 0: version (must be 1)
/// - byte 1: reserved (ignored)
/// - bytes 2-3: length in big-endian
pub fn parse_header(buf: &[u8]) -> Result<Header, ParseError> {
    if buf.len() < 4 {
        return Err(ParseError::TooShort);
    }
    let version = buf[0];
    if version != 1 {
        return Err(ParseError::InvalidVersion);
    }
    let length = u16::from_be_bytes([buf[2], buf[3]]);
    Ok(Header { version, length })
}

#[cfg(kani)]
mod proofs {
    use super::*;

    #[kani::proof]
    #[kani::unwind(5)]
    fn check_parse_header_no_panic() {
        let len: usize = kani::any();
        kani::assume(len <= 8);
        let buf: [u8; 8] = kani::any();
        let _ = parse_header(&buf[..len]);
    }
}

Kani verifica que parse_header nunca hace panic para cualquier buffer de entrada de longitud 0 a 8. Revisa el test de bounds, el check de versión y el indexado del array. Si hubiéramos escrito buf[1] en lugar de verificar la longitud primero, Kani encontraría un contraejemplo: un buffer de 1 byte donde buf[1] está fuera de bounds.

La annotation #[kani::unwind(5)] le dice a Kani cuántas veces desenrollar los bucles. Como nuestra función no tiene bucles, esto es conservador.

El problema del bounding: dónde el model checking choca con la pared

El model checking es exhaustivo dentro de sus límites. Fuera de esos límites, no dice nada. Este es el trade-off fundamental.

Los bucles son la primera pared. Kani debe desenrollar cada bucle un número fijo de veces. Si tu función itera sobre un Vec y pones el límite de unwind en 10, Kani prueba la corrección para vectors de longitud 0 a 10. No dice nada sobre la longitud 11. Cada incremento multiplica el espacio de estados. Un unwind de 50 podría terminar en minutos. Un unwind de 500 podría no terminar nunca.

La recursión es similar. Cada llamada expande la fórmula. La recursión profunda explota el uso de memoria.

El tamaño de los datos es la segunda pared. Kani maneja bien los arrays de tamaño fijo. Tiene problemas con colecciones asignadas dinámicamente a menos que acotes su tamaño explícitamente.

La standard library es la tercera pared. Kani modela mucho de ella, pero no todo. Si llamas algo que Kani no entiende, la prueba falla con una definición de función faltante.

Qué puede probar Kani y dónde falla

Kani es bueno encontrando panics, desbordamientos de enteros y violaciones de assertions en código acotado. Es excelente para primitivas criptográficas, parsers de protocol y pequeñas state machines. Son lugares donde una sola entrada mala causa catástrofe, y el código es naturalmente acotado.

Kani no es bueno probando propiedades de liveness, como “cada request eventualmente recibe una respuesta.” Eso requiere razonar sobre ejecuciones infinitas, lo que el bounded model checking explícitamente no hace. Para liveness, quieres un temporal model checker como TLA+.

Kani tampoco es un reemplazo para los tests. Una prueba que pasa te dice que no existe un contraejemplo dentro del límite. Un test te dice que el código se comporta correctamente para una entrada específica que te importa. Kani atrapa los edge cases en los que no pensaste. Los tests atrapan los problemas de integración que Kani no puede ver.

Corriendo Kani en CI sin derretir tus runners

Una sola prueba de Kani en una función pequeña toma segundos. Una suite en una crate real toma minutos. Una prueba con límites de unwind altos puede tomar horas. No quieres que tu pipeline de CI espere a un solve de SMT de dos horas.

Mantén las pruebas de Kani pequeñas y rápidas. Prueba las funciones safety-critical, las donde un bug es un incident. No intentes probar todo tu web framework. Pon un timeout, tal vez cinco minutos por prueba, y trata un timeout como un failure to prove, no como un proof of failure.

Aquí hay un patrón de Makefile que funciona:

# Makefile
kani:
	cargo kani --only-codegen --output-format=terse
	cargo kani --timeout 300 --all-functions --enable-unstable

kani-fast:
	cargo kani --only-codegen --output-format=terse
	cargo kani --timeout 60 --all-functions --enable-unstable

kani-fast corre en CI en cada pull request. kani corre por las noches. Si una prueba regresa, te enteras dentro de un día, no después de hacer ship.

Si expones una API pública, escribe una prueba de Kani por cada función pública que la llame con entradas completamente simbólicas. Esto es lo más cercano a un formal contract test. No prueba que la implementación sea correcta, pero prueba que la implementación no hace crash con entradas válidas arbitrarias.

Cuándo recurrir a un proof assistant real

Si necesitas probar propiedades sobre estructuras de datos no acotadas, como “esta linked list siempre es acíclica,” Kani no te ayudará. El límite de unwind anula el claim. Para esto, necesitas una herramienta como Creusot, que traduce Rust a WhyML y usa un proof assistant. Es más trabajo, pero maneja estructuras no acotadas.

Si necesitas pruebas de equivalencia o detección de undefined behavior, herramientas como MIRI o KLEE se sitúan en diferentes puntos del espectro effort-versus-coverage. Kani es el sweet spot para “tengo código acotado y quiero saber si hace panic.” Parsers, decoders, serializers y validadores de configuración encajan todos. El sistema de tipos de Rust ya elimina clases enteras de bugs. Kani elimina los que el sistema de tipos no puede alcanzar.

Qué probar primero

Si tienes una crate de Rust con una función que te da miedo, agrega Kani. La función que da miedo suele ser la que parsea untrusted input, hace manipulación de bits o indexa en arrays. Escribe un proof harness que la llame con kani::any(). Ejecuta cargo kani. Si pasa, tienes una prueba acotada de libertad de crashes. Si falla, tienes un contraejemplo concreto que habría sido un bug report.

No necesitas aprender un nuevo lenguaje. No necesitas entender cálculo de secuentes. Escribes assertions de Rust, y un solver te dice si se cumplen. Eso no es una prueba formal en el sentido académico. Es una prueba mecánica en el sentido práctico, y para la mayoría del software, práctico es exactamente lo que necesitas.

---

Preguntas frecuentes

¿Qué es el model checking en la verificación de software?

El model checking es una técnica automatizada que explora exhaustivamente todos los estados posibles de un sistema para verificar si las propiedades especificadas se cumplen. Para Rust, herramientas como Kani usan bounded model checking para probar assertions sobre todas las entradas posibles dentro de límites definidos, sin requerir construcción manual de pruebas.

¿En qué se diferencia Kani de escribir unit tests?

Un unit test revisa una entrada específica. Una prueba de Kani revisa cada entrada dentro de un límite. Si una prueba de Kani pasa, sabes que no existe un contraejemplo dentro del espacio de estados acotado. La prueba es más fuerte, pero está limitada por los límites que estableces.

¿Puede Kani probar que toda mi aplicación Rust es correcta?

No. Kani funciona mejor en funciones pequeñas y acotadas. El espacio de estados crece exponencialmente con las iteraciones de bucles, la profundidad de recursión y el tamaño de los datos. Usa Kani para componentes safety-critical como parsers y handlers de protocol, no para lógica a nivel de aplicación.

¿Qué pasa cuando Kani encuentra un bucle sin límite fijo?

Kani requiere un límite de unwind para los bucles. Si el bucle podría ejecutarse más veces de lo que permite el límite, Kani inserta una unwinding assertion que falla. Debes aumentar el límite o refactorizar el código para que tenga un conteo de iteraciones conocido estáticamente. Esta es la principal limitación del bounded model checking.