LO ESENCIAL EN 30 SEGUNDOS

  • PDD Kit traduce los requisitos acordados con el desarrollador a especificaciones de Verus; después, un agente debe escribir código Rust y pruebas que Verus acepte.
  • En una demo Pet Store de unas 5.000 líneas de Rust se demostraron cinco funciones de inicio de sesión, y seis componentes, como la comprobación bcrypt, quedan como confiables.
  • La herramienta es un prototipo de investigación que solo admite Rust; sus autores reconocen que las partes confiables concentran buena parte del riesgo restante.

Microsoft Research y GitHub Next han publicado un nuevo caso de estudio de PDD Kit, un prototipo de investigación basado en lo que denominan desarrollo guiado por pruebas formales. En lugar de confiar en tests que solo muestrean algunas entradas, el método pide a los agentes de programación que entreguen código Rust junto con demostraciones matemáticas, comprobadas por el verificador Verus, de que el código cumple una especificación formal para cualquier entrada permitida. El kit se presentó como versión preliminar de investigación en octubre; el trabajo más reciente lo aplica a una aplicación web completa.

De la intención revisada a la demostración

PDD Kit funciona dentro de Chopin, la herramienta de planificación de GitHub Next. Lee el código y plantea al desarrollador preguntas de revisor en «tarjetas de decisión», cuyas respuestas forman un documento de intención. Lo que puede formalizarse se convierte en precondiciones y poscondiciones de Verus. Un agente escribe después la implementación y su demostración, y Verus la verifica. Lo que no puede demostrarse debe nombrarse, ser aceptado por una persona y quedar cubierto por tests, que el proyecto presenta como evidencia y no como prueba. Dos agentes revisores contrastan la especificación con la intención, y un paso de mutación introduce un error por cláusula para confirmar que cada una restringe de verdad el código. Las pull requests resumen qué se demostró y qué se dio por confiable.

El experimento Pet Store

La aplicación de demostración es una tienda de mascotas de unas 5.000 líneas de Rust, con un backend en Axum y SQLite y una tienda en Leptos. El equipo se centró en el inicio de sesión, donde un fallo podría exponer cuentas de clientes o controles de administración, a partir de una petición de dos frases sobre la verificación de contraseñas y los tokens de administrador. El flujo de inicio de sesión asíncrono resultante tiene ocho poscondiciones; cinco funciones quedan demostradas y seis piezas siguen siendo confiables, entre ellas la comprobación bcrypt, dos consultas a la base de datos y la generación de tokens.

Límites que admiten los autores

Según la página del proyecto, PDD Kit solo funciona con Rust por ahora y escribir demostraciones sigue exigiendo un esfuerzo considerable. Las garantías dependen de los componentes confiables, que aún nadie ha demostrado. Las pruebas no cubren si el inicio de sesión termina, su velocidad, la limitación de peticiones ni los requisitos que nadie escribió. Además, una especificación puede ser válida sin reflejar lo que quería el desarrollador, así que la revisión humana sigue siendo necesaria. Los autores esperan que la zona confiable se reduzca con el tiempo, pero no han mostrado hasta dónde escala el método.