Tú revisas la especificación, la máquina revisa el código

GitHub Next y Microsoft Research anunciaron el Proof-Driven Development Kit el 21 de octubre. Está en vista previa de investigación, solo funciona en Rust, y plantea un argumento que la mayoría de los equipos con agentes de código han estado evitando: si ya no puedes leer el diff línea por línea, deja de fingir que puedes y revisa otra cosa.

Esa otra cosa es una especificación. En el flujo del PDD Kit, una persona aprueba la spec y una máquina comprueba que la implementación la cumple para todas las entradas posibles.

Cinco pasos, y dónde se sienta la persona

El bucle va así. Un equipo planifica la funcionalidad en Chopin, la herramienta de planificación agéntica multijugador de GitHub Next. Luego el PDD Kit discute el código, infiere la intención y propone una especificación formal escrita en Verus, un lenguaje de demostración de código abierto que ya existe para Rust. Una persona aprueba la spec, no el código. Después Verus demuestra que el código generado por el agente satisface esa spec para toda entrada. Donde no es posible una demostración completa, el kit recurre a tests y a agentes computer-use para una comprobación empírica, y la salida es un pull request verificado.

La inversión es toda la idea. Tú revisas el requisito. El verificador revisa la implementación. En Verus, una spec anota las funciones con precondiciones y postcondiciones que el verificador debe descargar, y la garantía es más fuerte que una suite de tests en verde de una forma concreta: los tests muestrean entradas, las demostraciones cuantifican sobre todas.

La formulación de GitHub es que Chopin más el kit permiten llevar código generado por IA a producción sin revisarlo línea por línea, con una garantía más fuerte que la revisión de código y los tests por sí solos. Eso es un proveedor describiendo su propia vista previa de investigación, no un resultado auditado. Tómalo con pinzas.

{{INLINE1}}

El costo se movió, no desapareció

Es tentador leer esto como «el problema de la revisión está resuelto». No lo está. Se movió al principio del pipeline, y se volvió más difícil de una forma fácil de subestimar.

Escribir una spec lo bastante precisa como para ser demostrable es una habilidad distinta de revisar un diff. Los requisitos vagos producen specs indemostrables, y el verificador te lo dirá fallando, así que las primeras semanas de adopción parecen las de una herramienta que no funciona. Lo que pasa en realidad es que la ambigüedad de tus requisitos sale a la superficie antes de lo habitual, empujada por algo que no la va a tapar con una función de aspecto plausible.

Para los equipos que ya escriben documentos de diseño que nadie lee, esto es un cambio real. El documento de diseño pasa a ser estructural, porque es el artefacto que se comprueba.

Dónde se detienen las demostraciones

Hay tres límites que importan más que la lista de funciones.

Solo Rust. Verus comprueba Rust, y GitHub Next dice que el kit funciona hoy en Rust, sin lenguaje nuevo y sin cambiar cómo se produce el código. Si tus agentes escriben TypeScript o Python, todavía no hay nada que instalar. Teniendo en cuenta cuánto código de producción no es Rust, es una restricción enorme metida en una frase pequeña.

Solo lo que una spec puede expresar. La demostración formal cubre propiedades que puedes enunciar con precisión: contratos de entrada y salida, invariantes, transiciones de máquina de estados. No cubre el comportamiento de la interfaz, ni la mayor parte de la lógica con mucha entrada y salida, ni nada donde lo correcto sea un juicio y no una propiedad. Todo eso baja al camino de respaldo de tests y revisión humana, que es exactamente donde ya vive la carga de hoy.

Vista previa de investigación, con una historia concreta. Chopin figura en la página de proyectos de GitHub Next como prototipo de investigación fechado en septiembre de 2026. GitHub Next ya ha publicado prototipos antes —Repo Mind, Project Copernicus, SpecLang entre ellos— que nunca llegaron a disponibilidad general. La primera demo pública sobre código real está agendada para GitHub Universe, el 28 y 29 de octubre.

La honestidad está en el camino de respaldo

La decisión de diseño que más dice no es el demostrador. Es el segundo camino explícito para el código que no se puede demostrar, que va a tests y agentes computer-use para comprobación empírica.

Es una admisión que la mayoría de las herramientas de verificación se niegan a hacer. Dice, en la arquitectura, que hay código demostrable y código que no, y que fingir lo contrario sería peor que enviar dos pipelines. Un equipo que usa esto acaba con una etiqueta por módulo —demostrado, testeado, revisado—, que es un inventario de confianza más honesto que cualquier cosa que produzca un informe de cobertura.

El problema es que el camino de respaldo es también donde los agentes se corrigen su propia tarea. Un agente computer-use que hace clic por una interfaz para comprobar si un cambio funcionó sigue siendo un agente, sigue muestreando y sigue siendo capaz de concluir que un flujo roto se ve bien. El camino demostrado da una demostración. El respaldo da una demo que pasó.

La investigación de fondo es la parte tranquilizadora

El kit no es un verificador construido desde cero. Verus es independiente y está consolidado. El repositorio verus-proof-synthesis de Microsoft Research contiene los cimientos: dos sistemas impulsados por LLM, AutoVerus y VeruSAGE, que generan y reparan demostraciones de Verus, evaluados contra 150 y 849 tareas de verificación respectivamente.

Lo que el kit parece añadir es empaquetado. Es la primera vez que esta línea de investigación en síntesis de demostraciones se pliega en un flujo de producto que va del plan al PR en lugar de un ejercicio de benchmark. Es una afirmación más pequeña que «la IA puede demostrar su propio código», y más creíble.

Ojo también con que las fuentes no se ponen de acuerdo en el nombre. Verás Proof-Driven Development Kit y Property-Driven Development Kit en la cobertura de la misma semana, ambos atribuidos al mismo anuncio. Elige uno y sigue; el acrónimo hace el branding en cualquier caso.

Lo que puedes hacer hoy

La conclusión que perdura no es «espera al GA». Es que un código con muchos agentes ahora se parte en territorio demostrable y no demostrable, y tu configuración ya debería saber cuál es cuál.

Parsers, máquinas de estados, invariantes de estructuras de datos, aritmética con cotas, primitivas de concurrencia: eso es territorio demostrable, y Verus es código abierto y se puede usar ya, con o sin el kit. La mayor parte del trabajo de front-end, la mayor parte del código pegamento y todo aquello cuya corrección depende de qué quiso decir un usuario, no.

Se siguen dos movimientos prácticos. Primero, etiqueta los módulos demostrables de tu repositorio y apunta a tus agentes a Verus solo para esos, antes de que ningún proveedor publique un flujo. Segundo, deja de pedirle a los agentes que además escriban los tests que validan su propio trabajo; ese arreglo siempre ha sido un conflicto de interés, y es la razón por la que una suite en verde significa menos que antes.

La pregunta incómoda

Si una spec la puede aprobar una persona y una demostración la puede descargar una máquina, ¿para qué exactamente está el revisor? No para leer código, y probablemente no para atrapar el bug que el agente metió en la línea 412.

El trabajo del revisor pasa a ser el que siempre debió ser: decidir qué se supone que hace el sistema y negarse a aceptar una especificación que no lo diga. Eso es más difícil que pulsar aprobar en un diff. También es la única parte del trabajo que un verificador no puede hacer por ti.