PDD Kit es un prototipo de investigación que convierte requisitos de software en contratos formales y comprueba si el código escrito por agentes los cumple. Importa porque permite definir con precisión qué comportamiento se quiere exigir, aunque la prueba solo cubre lo expresado en esos contratos y las entradas incluidas en el modelo.
Qué verificó PDD Kit en Pet Store
En una publicación del 5 de noviembre de 2026, Microsoft Research describió PDD Kit y una demostración centrada en el inicio de sesión de Pet Store, una aplicación completa escrita en Rust. La demostración informa de pruebas formales para cinco funciones: login_flow, login_core, lookup_target, decide_login e issue_token. Sus cuerpos cumplen los contratos definidos para todas las entradas representadas en el modelo, según Microsoft Research.
El contrato de login_flow tiene ocho cláusulas ensures, que expresan condiciones que deben cumplirse. Entre ellas figuran la relación entre la cuenta y el token, las condiciones de contraseña, las restricciones de rol y las respuestas de error previstas. Esas ocho cláusulas corresponden a login_flow, no a toda la aplicación: el ejemplo verifica la lógica de inicio de sesión, no Pet Store de punta a punta.
Cómo una intención se convierte en una condición comprobable
Una especificación formal expresa en términos precisos qué debe hacer el programa. En el flujo descrito, la intención se revisa, las decisiones sobre requisitos ambiguos quedan registradas y el agente genera código y contratos para que Verus los compruebe.
El ejemplo de la contraseña muestra por qué importa concretar el requisito. «No emitir un token si la contraseña es incorrecta» impide los accesos indebidos, pero también permitiría un sistema que rechazase a todo el mundo. Añadir que la contraseña correcta debe permitir el inicio de sesión descarta esa posibilidad. El contrato contempla un error si el hash almacenado no se puede leer.
La tarjeta de decisión de PDD Kit plantea precisamente si una contraseña correcta debe producir siempre un token y compara dos formas de expresar esa promesa.
Qué queda bajo confianza y se comprueba con tests
Una prueba formal demuestra que el código satisface las propiedades escritas en la especificación para las entradas que contempla el modelo. Un test ejecuta casos concretos. En el ejemplo de Pet Store, Microsoft Research separa seis categorías de operaciones confiables; una agrupa dos consultas a la base de datos. Las consultas, la verificación de contraseñas con bcrypt, la firma de tokens, el acceso al reloj, el tratamiento de errores de base de datos y la extracción de datos de la solicitud se aceptan mediante contratos y se someten a tests, no se demuestra formalmente la implementación externa de cada operación.
Eso delimita el resultado: la prueba cubre las funciones y condiciones especificadas, mientras que los componentes confiables dependen de sus propios contratos y pruebas. El ejemplo tampoco garantiza que el inicio de sesión asíncrono termine ni cuánto tardará.
Una prueba formal verifica el contrato escrito; no decide si ese contrato recoge todos los requisitos que el equipo quería expresar.
Por qué una prueba no valida por sí sola los requisitos
El código puede cumplir un contrato incompleto o equivocado. La revisión de requisitos ayuda a detectar ambigüedades, pero el resultado formal no demuestra por sí mismo que la especificación represente toda la intención del desarrollador.
En un artículo fechado el 17 de marzo de 2026, Shuvendu K. Lahiri sitúa las pruebas y los contratos ejecutables en un extremo de un espectro de formalización; después aparecen los contratos lógicos, como los de Verus, y la síntesis verificada mediante lenguajes específicos de dominio. El trabajo identifica la validación de especificaciones como un problema central: no hay un criterio independiente que capture por completo lo que una persona quiso decir. Este marco más amplio ayuda a entender el lugar de PDD Kit, sin cambiar el alcance de la demostración de Pet Store. (Artículo de Lahiri.)
Qué aporta Verus y por qué el ejemplo usa Rust
Microsoft Research describe el prototipo de PDD Kit como una herramienta para verificar código Rust. Verus, el verificador que emplea, usa métodos SMT, es decir, técnicas que comprueban fórmulas con ayuda de teorías matemáticas. Su descripción oficial de Verus explica que las especificaciones y pruebas aprovechan la sintaxis de Rust, sus tipos lineales y el comprobador de préstamos (borrow checker) para razonar sobre la propiedad y separación de recursos.
Microsoft Research recomienda comenzar por componentes de alto riesgo y ampliar el trabajo de forma gradual: las pruebas formales requieren esfuerzo, y el prototipo descrito se limita a Rust.
