La tecnología de verificación de Rust aplicada al código de sistemas de bajo nivel

Verus: una herramienta para verificar la corrección del código Rust

• Verus es una herramienta para verificar la corrección del código escrito en Rust.
• El desarrollador escribe la especificación de lo que el código debe hacer, y Verus verifica estáticamente si el código ejecutable en Rust siempre cumple la especificación para todas las ejecuciones posibles del código.
• En lugar de agregar verificaciones en tiempo de ejecución, Verus depende de un solver potente para demostrar que el código es correcto.
• Verus admite actualmente un subconjunto de Rust (en expansión) y, en algunos casos, permite que el desarrollador verifique estáticamente la corrección del código más allá del sistema de tipos estándar de Rust (por ejemplo, la manipulación de punteros crudos).

Estado actual de Verus

• Verus está en desarrollo activo
• Es posible que se rompan o falten funciones, y la documentación sigue siendo incompleta.
• Si vas a probar Verus, debes estar listo para pedir ayuda en Zulip.

Probar Verus

• Para probar Verus desde el navegador, visita Verus Playground.
• Para un desarrollo más complejo, sigue las instrucciones de instalación y revisa los documentos a continuación, comenzando por tutoriales y referencias.

Documentación de Verus

• Tutoriales y referencias
• Documentación API de la biblioteca estándar de Verus
• Guía para verificar código concurrente
• Objetivos del proyecto
• Contribuir a Verus
• Licencia

Contactar, reportar problemas y comenzar una discusión

• Reporta issues, inicia una discusión o únete a Zulip para discutir y recibir ayuda en tiempo real.
• Usa los issues de GitHub para errores (problemas ejecutables) existentes y GitHub Discussions para solicitudes de funciones y conversaciones más abiertas sobre características planificadas.
• Las contribuciones son bienvenidas. Si quieres contribuir con código, revisa los tips para contribuir a Verus.

Opinión de GN⁺

• Rust es conocido como un lenguaje adecuado para programación de sistemas, que garantiza seguridad y rendimiento; Verus se presenta como un proyecto que puede potenciar aún más esas ventajas de Rust. En particular, su soporte para la verificación de programación concurrente parece muy interesante.

• Sin embargo, todavía está en una etapa temprana y parece que la sintaxis de Rust compatible es limitada, por lo que parece requerir más desarrollo para usarlo en producción real. Pero, dado que la seguridad del código se garantiza de forma preventiva mediante análisis estático, su potencial de evolución es alto.

• Aunque aún necesita mejoras como documentación insuficiente y soporte sintáctico limitado por su fase inicial, es probable que llegue a ser un proyecto importante en el ecosistema de Rust a largo plazo. En particular, se espera que su uso sea alto en áreas donde la confiabilidad es crítica, como programación de sistemas o blockchain.

[GN⁺]

Comentarios de Hacker News

• Se escribió un controlador de Kubernetes formalmente verificado usando Verus
  • Puede demostrarse una propiedad de liveness de que el controlador finalmente ajustará el clúster al estado deseado solicitado
  • Hay muchos matices al especificar la corrección (cambios rápidos en los requisitos del estado deseado, asincronía, fallos, etc.)
  • El código está en GitHub y está enlazado con un paper que se publicará en OSDI 2024
• Un pequeño paso hacia Verus: se pueden agregar precondiciones y postcondiciones con debug_assert de Rust
  • El compilador de Rust los elimina por defecto en compilaciones de producción
  • Hay ejemplos del tutorial de Verus y ejemplos de comprobaciones en tiempo de ejecución con debug_assert
• Pregunta de principiante sobre la diferencia entre "verificación de la corrección del código" y "demostración de la corrección del código"
  • Tiene curiosidad por buenos recursos de aprendizaje para "probar código" dirigidos a desarrolladores de software con poca base en CS/matemáticas
  • Está muy intrigado por qué las pruebas de "conocimiento cero" son tan importantes y por qué están tan relacionadas
• Rust todavía no tiene un estándar como C/C++, Common Lisp o Ada/SPARK2014
  • Eso lo convierte en un objetivo dinámico frente a herramientas de verificación desarrolladas para Ada/SPARK2014, entre otras
• Dafny es un lenguaje de programación "consciente de verificación" que se puede compilar a Rust (GitHub)
• Uno de los principales contribuidores dio una excelente charla sobre Verus en un meetup de Rust en Zúrich (YouTube)
  • Lo que más llamó la atención fue lo bien que el código "ghost" encaja en el programa (me recordó un poco a Ada)
• Comparativa entre Verus y SPARK
  • ¿Es una familia de verificadores del mismo tipo? ¿Qué diferencias hay además de que Verus sea un verificador para Rust y no para Ada?
• ¿Alguien experto en Verus puede comparar el rendimiento y la expresividad entre Verus y Lean4?
  • Entiendo que Verus es una herramienta de verificación basada en SMT y que Lean es un asistente de demostración interactivo además de una herramienta basada en SMT
  • Sin embargo, como mi entendimiento de la verificación formal es limitado, sería útil escuchar la opinión de alguien experto en técnicas formales de software
• ¿Verus tiene relación con Kani? ¿Funcionan de forma distinta? (GitHub de Kani)
• ¿Existe una forma de implementarlo para que el código resultante siga siendo Rust válido y pueda compilarse con las herramientas de Rust estándar?