La brecha entre el código correcto y un programa verificado

Los LLMs pueden escribir Rust que compila e incluso pasa cargo test. Lo que no pueden hacer de forma confiable es escribir una prueba formal de que el código es correcto para todas las entradas posibles.

El problema no es la sintaxis de Rust. La verificación formal requiere establecer lo que quieres probar, encontrar la invariante que hace que la prueba funcione, y expresar ambas cosas en un lenguaje que el verificador acepte. Los LLMs se entrenan con código fuente, no con el acto de probar. Ven teoremas, pero rara vez ven los veinte intentos fallidos que precedieron a la prueba exitosa.

Si pegas una búsqueda binaria recursiva en GPT-4 y le pides que “pruebe que esto es correcto”, obtendrás algo que parece una prueba. Mencionará invariantes de bucle y precondiciones. También probablemente usará sintaxis de Dafny, referenciará lemas que no existen, y afirmará invariantes que son demasiado débiles para establecer la postcondición. Parece correcto hasta que intentas verificarlo.

Cómo se ve en realidad la verificación formal de Rust

Rust tiene varias herramientas de verificación. Kani es un model checker que explota exhaustivamente todos los estados posibles de una función hasta cierto límite. Prusti y Creusot son verificadores deductivos que traducen Rust a lógica y le piden a un SMT solver que pruebe propiedades. Cada uno requiere anotaciones en una sintaxis específica.

Aquí hay una función simple y cómo se ve una prueba deductiva real en Creusot:

// Requires creusot-contracts crate
use creusot_contracts::*;

#[requires(a.len() > 0)]
#[ensures(result == a[0])]
pub fn first<T>(a: &[T]) -> &T {
    &a[0]
}

Creusot verifica que la precondición a.len() > 0 garantiza la postcondición result == a[0]. Esto es trivial porque la lógica es simple. Ahora hagámoslo más difícil:

use creusot_contracts::*;

#[requires(n <= 1000)]
#[ensures(result == n * (n + 1) / 2)]
pub fn sum_to(n: u32) -> u32 {
    let mut i = 0;
    let mut s = 0;
    #[invariant(i <= n)]
    #[invariant(s == i * (i + 1) / 2)]
    while i < n {
        i += 1;
        s += i;
    }
    s
}

Las invariantes son la parte difícil. Un humano las escribe pensando en qué permanece verdadero en cada iteración. Un LLM podría adivinar s == i * (i - 1) / 2 porque ese patrón aparece en los datos de entrenamiento, o podría omitir la invariante por completo y dejar que el solver falle.

Qué sucede cuando le pides una prueba a un LLM

Probé esto con varios modelos. El prompt fue: “Escribe una función verificada en Rust que calcule el factorial de n usando Creusot, con precondiciones, postcondiciones e invariantes de bucle completas.”

Las respuestas cayeron en tres categorías.

Primero, algunos modelos produjeron anotaciones que parecían plausibles pero usaban la sintaxis incorrecta. Escribieron #[precondition(...)] en lugar de #[requires(...)], o mezclaron sintaxis de Prusti con sintaxis de Creusot. El código ni siquiera parseaba.

Segundo, algunos modelos produjeron anotaciones sintácticamente correctas con invariantes que eran demasiado débiles. La función factorial necesita una invariante como res == fact(i). Los modelos a menudo escribieron res >= i, que es verdadero pero inútil para probar la postcondición. Creusot reportaría que no podía establecer el objetivo, y el LLM no tenía mecanismo para corregirlo.

Tercero, algunas respuestas acertaron la invariante pero alucinaron un lema auxiliar. Referenciaban una función math::fact que no existe en la biblioteca estándar de Creusot. La prueba solo funciona si construyes tú mismo esa definición lógica.

Ninguno de los modelos produjo una prueba que pasara a la primera.

Dónde los LLMs realmente ayudan en el flujo de verificación

Esto no significa que los LLMs sean inútiles para la verificación formal. Significa que debes usarlos para las tareas correctas.

Son buenos generando boilerplate. Dada una firma de función, un LLM usualmente puede producir las cláusulas #[requires] y #[ensures] que capturan los contratos obvios. Para una función fn divide(a: i32, b: i32) -> i32, sugerirá correctamente #[requires(b != 0)] y #[ensures(result * b == a)]. Estas no son ideas profundas, pero ahorran pulsaciones de teclas.

Son decentes explicando errores del verificador. Si Creusot reporta “cannot prove loop invariant”, pegar el error en un LLM suele dar una explicación útil de lo que se supone que debe hacer la invariante. No sugerirá la invariante exacta que necesitas, pero reducirá el espacio de búsqueda.

Son útiles para traducir entre lenguajes de verificación. Si tienes una prueba en Dafny y quieres portarla a Prusti, un LLM puede manejar gran parte del mapeo sintáctico. La lógica subyacente es la misma. Este es exactamente el tipo de tarea de reconocimiento de patrones en la que los LLMs destacan.

La limitación fundamental: probar es búsqueda, no completado

Escribir una prueba no es como escribir un servidor web. Cuando escribes un servidor web, hay muchas respuestas correctas. Cuando escribes una prueba, hay exactamente una respuesta, o una pequeña familia de respuestas, y todo lo demás está mal.

Los LLMs son predictores de siguiente token. Generan la continuación más probable dado el contexto. Un paso de prueba no es la continuación más probable. Es el paso que cierra la obligación de prueba, que puede ser la vigésima opción más probable o la dosmilésima.

Considera probar que una función de ordenamiento devuelve una permutación de su entrada. La idea clave suele ser definir un multiset o contar ocurrencias. Un LLM podría sugerir comparar longitudes, que es necesario pero no suficiente. Se necesita un humano para reconocer que la igualdad de longitudes no implica permutación, e introducir la invariante de conteo.

El model checking con Kani evita algo de esto porque no requiere invariantes. Los LLMs pueden generar harnesses de kani::proof de forma más confiable porque se parecen a unit tests. Pero Kani solo funciona para verificación acotada. Si necesitas una prueba no acotada, aún necesitas al humano.

Un flujo de trabajo práctico que usa ambos

Si quieres verificar Rust hoy, aquí hay un flujo de trabajo que realmente funciona.

Empieza escribiendo el código normalmente. Ejecuta cargo test. Luego añade contratos. Usa un LLM para generar las cláusulas #[requires] y #[ensures] a partir de la firma de la función. Revísalas cuidadosamente. El modelo acertará las fáciles y las difíciles las errará sutilmente.

Ejecuta el verificador. Fallará al menos en un bucle. Toma el mensaje de error y pídele al LLM que explique qué invariante falta. Usa su explicación como punto de partida, no como respuesta. Escribe la invariante tú mismo.

Itera. El verificador te dirá si tu invariante es lo suficientemente fuerte. El LLM no lo hará. Trata al modelo como un programador par que conoce la sintaxis pero nunca ha terminado una prueba.

La respuesta honesta a la pregunta

¿Pueden los LLMs escribir pruebas formales para Rust? No. Todavía no. No sin un humano que entienda la lógica.

Pueden escribir el andamiaje, explicar errores y traducir entre herramientas. Pero encontrar la invariante, el lema o la hipótesis de inducción que hace que la prueba funcione sigue siendo una habilidad humana.

Si buscas una herramienta que te permita saltarte el aprendizaje de separation logic o Hoare triples, un LLM no lo es. Si buscas una herramienta que haga la curva de aprendizaje menos empinada manejando la sintaxis y el boilerplate mientras te enfocas en la lógica, un LLM vale la pena probarlo.

Empieza con Kani si quieres verificaciones acotadas sin invariantes. Pasa a Creusot o Prusti cuando necesites pruebas no acotadas. Usa el LLM para acertar la sintaxis, pero espera escribir la prueba tú mismo.

Preguntas frecuentes

¿Qué es la verificación formal en Rust?

La verificación formal usa lógica matemática para probar que un programa satisface una especificación para todas las entradas posibles. En Rust, herramientas como Kani, Prusti y Creusot añaden anotaciones a las funciones que describen precondiciones, postcondiciones e invariantes. Un verificador luego comprueba si estas propiedades se cumplen.

¿Puede ChatGPT escribir pruebas para Kani?

ChatGPT puede escribir harnesses de prueba de Kani, que se parecen a unit tests con atributos #[kani::proof]. Estos harnesses son más fáciles de generar que pruebas deductivas porque no requieren invariantes de bucle. Sin embargo, los harnesses complejos con assumptions y assertions aún necesitan revisión humana.

¿Cuál es la diferencia entre Kani y Creusot?

Kani es un bounded model checker. Explota todos los caminos de ejecución posibles hasta un límite y comprueba panics o fallos de assertion. Creusot es un verificador deductivo. Traduce Rust a fórmulas lógicas y usa un SMT solver para probar propiedades para todas las entradas, incluyendo bucles no acotados, pero requiere invariantes proporcionadas por el usuario.

¿Por qué los LLMs tienen dificultades con las invariantes de bucle?

Las invariantes de bucle requieren razonar sobre qué permanece verdadero a través de iteraciones, lo cual es una forma de razonamiento inductivo. Los LLMs se entrenan para predecir continuaciones de texto probables, no para buscar la declaración lógica exacta que cierra una obligación de prueba. La invariante correcta a menudo no es el siguiente token más probable.