Verus es un verificador de programas automatizado y de código abierto diseñado para garantizar la corrección matemática del código escrito en Rust. A diferencia de las pruebas tradicionales, que pueden omitir casos límite, Verus utiliza especificaciones formales para demostrar que el código cumple sus requisitos para todas las entradas posibles. Esta herramienta es particularmente útil en proyectos críticos de Amazon, como el motor de aislamiento de máquinas virtuales Nitro, donde se ha utilizado para probar la corrección de primitivas clave y componentes de infraestructura.
El sistema se integra directamente en los archivos de fuente de Rust mediante anotaciones que definen precondiciones y postcondiciones. Al escribir las pruebas en el mismo lenguaje que el código, los desarrolladores pueden ver mensajes de error en tiempo real, lo que facilita un ciclo de desarrollo interactivo. Verus emplea solvers para automatizar la construcción de pruebas, permitiendo verificar proyectos complejos con miles de líneas de código en segundos. Además, la herramienta permite demostrar la seguridad de código marcado como 'unsafe' y la corrección de código concurrente, complementando las garantías de seguridad del sistema de tipos de Rust. Esta combinación de verificación formal y automatización rápida ofrece una capa adicional de fiabilidad para sistemas que requieren un alto nivel de precisión y seguridad.