Investigadores han presentado Verus, una nueva herramienta diseñada para verificar la corrección del código escrito en Rust. El objetivo principal es asegurar la funcionalidad completa de código de sistemas de bajo nivel, basándose en principios de lenguajes de verificación existentes como Dafny, Boogie y F*. Verus utiliza un lenguaje matemático para expresar especificaciones y pruebas, y un lenguaje de bajo nivel basado en Rust para el código ejecutable. La herramienta genera condiciones de verificación que pueden ser resueltas eficientemente por un solucionador SMT como Z3, aprovechando las características avanzadas del sistema de tipos de Rust, incluyendo tipos lineales y borrowing para simplificar el razonamiento sobre la memoria. Los desarrolladores no pretenden soportar todas las características de Rust inicialmente, sino enfocarse en aquellas de alto valor para sus usuarios. El uso de Verus requiere familiaridad con Rust, aunque la herramienta extiende la sintaxis de Rust con nuevos conceptos para la especificación y la prueba, y ofrece tutoriales para guiar a los usuarios a través de la verificación de código, desde ejemplos básicos hasta pruebas más complejas que involucran concurrencia.
Noticias agregadas con IA