Verus, el verificador open source que demuestra que tu código Rust es correcto

Verus es un verificador de programas automático y open source para Rust, y Amazon lo pone como la pieza que lleva el lenguaje un paso más allá de su sistema de tipos. La idea: no basta con que el compilador te libre de una buena parte de los bugs; se trata de demostrar matemáticamente que el código hace lo que dijiste que haría, para cualquier entrada posible.

El argumento de partida lo conocen bien quienes escriben Rust. En C, indexar fuera de los límites de un array es un error con consecuencias imprevisibles; en Rust el programa se detiene, lo cual es más seguro, pero un programa correcto no accedería nunca ahí. Tampoco garantiza el sistema de tipos que el resultado sea el esperado ni que el código no filtre secretos a los que tiene acceso. Eso queda para la verificación formal.

Un verificador de este tipo coge una especificación matemática del comportamiento esperado y comprueba de forma mecánica que el código la cumple para todas las entradas. El ejemplo que usa el equipo es una búsqueda binaria: la especificación puede exigir que, si la función devuelve un índice, el elemento en esa posición sea el valor buscado, y que si devuelve None, el valor no esté en el array. Los tests clásicos prueban unos cuantos arrays y se dejan casos de esquina; la verificación cubre todos.

Especificaciones dentro del propio Rust

Lo que distingue a Verus de otros enfoques es dónde se escriben las pruebas. El desarrollador añade especificaciones y demostraciones directamente en los ficheros fuente de Rust, con sintaxis parecida al propio lenguaje: la palabra clave requires para las precondiciones y ensures para las postcondiciones. El compilador normal ignora esas anotaciones, así que el mismo código sirve para proyectos verificados y sin verificar, Cargo incluido. Cuando una prueba falla, el error llega como un mensaje al estilo de Rust, a nivel de código fuente.

Verus reparte las obligaciones de prueba entre varios solvers. En la práctica, el desarrollador recibe respuesta en menos de un segundo, lo justo para mantener el bucle interactivo con subrayados en editores como VS Code. A escala de proyecto, la herramienta verifica miles de líneas de código y de prueba en el tiempo que verificadores anteriores empleaban en funciones sueltas.

Amazon ya lo usa en el Nitro Isolation Engine

Amazon es miembro fundador de la Rust Foundation y usa el lenguaje en Firecracker, que sostiene Lambda y Fargate, y en el Nitro Isolation Engine, que aplica el aislamiento de máquinas virtuales en el hipervisor Nitro. Según la compañía, Verus ya ha servido para demostrar la corrección de primitivas clave del Isolation Engine y de otras piezas de infraestructura interna. Son afirmaciones suyas y el material no incluye cifras ni comparativas de rendimiento.

Que un gigante con más de una década de trabajo en razonamiento automatizado meta verificación formal en su código de producción dice por dónde va una parte de la ingeniería de sistemas: menos confiar en que los tests pasen y más demostrar que no pueden fallar. Queda por ver cuánto de ese flujo sobrevive al día a día de un equipo corriente, donde escribir especificaciones compite con entregar. El código está en su repositorio.