Decirle TDD al agente no lo hace verificador

El Cuñado dice: "Le pones en el prompt que use TDD, Lean 4 y property-based testing y ya verifica solo. El QA sobra. En seis meses esto lo hace un agente."

La realidad es: Dan Luu lo midió. Instrucciones simples a un agente de código, "usa TDD", "usa Lean 4", "usa QuickCheck", "usa property-based testing", y ninguna técnica disparó la corrección de forma decisiva. La condición Default, sin ninguna instrucción extra de testing, quedó por encima de la media del eval.

Por qué importa saberlo: el plan de agente autónomo fiable que consiste en nombrarle el método compra teatro. El agente cambia la etiqueta de los tests que ya escribía. Sigue sin distinguir una verificación que vale de un gesto vacío.

Lo que se midió de verdad

Luu reutilizó un eval de implementación de Zstd, todo en Rust. No estaba juzgando si TDD funciona cuando lo practica alguien que sabe qué test merece la pena, ni si Verus rinde en un equipo que vive de métodos formales. La pregunta era más cutre y más útil: si le sueltas el nombre de la técnica a un agente, ¿sale una implementación más correcta?

La herramienta: codex con GPT-5.6 Sol, en esfuerzos medium y xhigh. De media, 80 ejecuciones por condición. La métrica es seca: fracción de runs que pasan el 100% de los tests ocultos, puesta al lado del coste. Encima evaluó cuatro skills de testing externas y una propia.

El resultado central no da para ranking. Ninguna técnica de test o verificación deja a las demás en ridículo. Ninguna instrucción simple dispara la corrección. En xhigh, fuzzing y property-based testing quedaron un poco mejor que los métodos formales de media; en medium el asunto se mezcla de verdad. Campeón claro, ninguno.

Default, por encima de la media

Ahí está el hostiazo. Dar el nombre de una técnica no mejoró lo que el agente hace por defecto. Default se sitúa por encima de la media del eval.

Añadir ceremonia con nombre famoso no empuja el resultado hacia arriba. A menudo lo que haces es distraer al modelo para que rellene el marco de la escuela que le has nombrado, con el mismo criterio de siempre y un disfraz más caro.

Luu lo resume sin poesía. En general los agentes no saben usar bien estas herramientas ni estas técnicas. Son malos testeando por defecto. Todo el que ha consultado le dice lo mismo: sin guía experta no entienden cómo testear de forma razonable.

Cuando nombra una técnica, el agente escribe los mismos tests de siempre dentro de ese framework, o la usa de forma superficial, sin hacer lo que extrae su valor.

Verus prueba que A implica A

Con Verus no verificaron el código real. Probaron propiedades abstractas e irrelevantes sobre Zstd. Escribieron pocas pruebas y, a menudo, vacuas: el equivalente formal de A ⇒ A. Tener la documentación de la herramienta no les sacó valor por sí sola.

Una tautología viste de verificación. El comprobador asiente, el agente marca la casilla y no has dicho nada del compresor. Has dicho que una cosa es igual a sí misma y lo has llamado prueba.

// el "teorema" que no toca el bug
assert!(decoded == decoded); // A ⇒ A

El property-based testing sale igual de hueco por otro lado. En vez de elegir propiedades que romperían el código si fallan, se apoyaron en inputs totalmente aleatorios. Castigaron casos de rechazo inválidos. Verificaron propiedades triviales con casos de bajo valor. El generador tira dados. El bug de transposición, el del estado, el del bitstream que no es el que crees, ni se entera.

TDD no fue bien, y Luu lo había apuntado antes de correr el eval, con un 55% de confianza pre-registrada. Una skill que además instruía a usar TDD también fue mal en los casos en que los agentes siguieron la instrucción. Eso no convierte TDD en una estafa para humanos. Convierte el ciclo red-green en otra pegatina cuando quien lo ejecuta no tiene criterio para el test rojo que importa.

En xhigh los agentes lograban pasar los tests que ellos mismos escribían. Los tests eran pobres. Un ejemplo que duele de lo concreto: cuatro bitstreams idénticos en una feature que usa cuatro, sin detectar bugs de transposición. Si cambias el orden de los cuatro y el test sigue verde, no tienes cuatro casos. Tienes uno copiado.

Ese es el agujero operativo. El valor esperado de un test no puede salir de ejecutar el código que se está juzgando. Tiene que salir de un contrato que el agente no pueda reescribir a su favor. Si el mismo sistema genera la implementación y el oráculo, el oráculo es un espejo. Los tests ocultos del eval, los que el agente no ve, son lo único que aquí hace de suelo. Los que escribe él, no.

El harness decide el número que publicas. Aquí el instrumento interno del agente está sesgado de fábrica: optimiza para ponerse verde a sí mismo.

Tampoco es cosa de Zstd

Por si alguien sale con que comprimir bits es un dominio raro y por eso el agente se pierde: los resultados no fueron materialmente distintos en el eval del RFC de IMAP, con 40 ejecuciones por condición, ni en otros RFCs. El mal uso de las técnicas se repite en problemas de protocolo. No es un capricho del bitstream. Rellenan el marco en IMAP con la misma cara de póker que en Zstd.

La skill de 250.000 estrellas rinde peor que la media

Luu no se quedó en el prompt de una línea. Metió skills de testing. Las que recomendó codex, incluida una skill ECC con 250.000 estrellas en GitHub, rindieron peor que la media. Estrellas en el repo no son criterio de verificación.

La skill propia, hecha rápido y diseñada para empujar al agente fuera de su comportamiento por defecto, funcionó razonablemente. Ahí está el contrapunto que hay que dejar escrito, no el de consuelo.

Este eval no demuestra que fuzzing, PBT o métodos formales sean inútiles. Demuestra que estos agentes no los aplican bien con una instrucción simple. El margen, si existe, está en cómo se les guía: un artefacto pensado para sacarlos de la rutina vio señal; pegar el nombre de una escuela, no.

Eso también recorta la fantasía del AI Engineer que en realidad es prompteador con autoestima. No porque el prompt no importe, la skill propia importó, sino porque importar no es copiar "usa TDD" de un hilo. El trabajo es empujar al modelo fuera de los tests que ya iba a escribir.

El cuello de botella es el criterio

Las técnicas que Luu nombra existen porque, usadas en serio, obligan a declarar una propiedad: qué tiene que seguir siendo verdad cuando el input se tuerce, qué invariante no puede romper un refactor, qué equivalencia no es un A ⇒ A. El agente no trae ese modelo mental. Trae la sintaxis del framework.

Por eso Default puede quedar por encima. El comportamiento por defecto ya era mediocre. Nombrar la técnica no le injerta juicio. Le injerta un disfraz. Y el disfraz cuesta atención y un falso positivo de rigor: "he usado Verus".

Si de verdad quieres verificación y no teatro, el movimiento no es alargar el system prompt. Es decidir qué no puede editar quien escribe el código. El oráculo. Los tests ocultos. El contrato de la propiedad. Separar quien implementa de quien comprueba no es un capricho de grafos: es la condición para que el test deje de ser un selfie.

Los tests ocultos siguen siendo el único adulto en la sala.

Preguntas frecuentes

¿Mejora el código decirle a un agente que use TDD o Lean 4?

No: en el eval de Dan Luu ninguna instrucción simple de testing disparó la corrección de forma decisiva. Probó TDD, Lean 4, QuickCheck y property-based testing con codex y GPT-5.6 Sol. La condición Default, sin esas instrucciones, quedó por encima de la media. El agente escribe los mismos tests de siempre dentro del framework o usa la técnica de forma superficial.

¿Hay alguna técnica de verificación que los agentes usen claramente mejor?

No hay una técnica ganadora clara. En esfuerzo xhigh, fuzzing y property-based testing rindieron un poco mejor que los métodos formales de media; en medium el panorama fue mucho más mixto. Ninguna "wildly outperforms" a las demás. Nombrar el método no basta para extraer el valor de la herramienta.

¿Eso significa que TDD o Verus no sirven?

No. El eval no demuestra que las técnicas sean inútiles, solo que estos agentes no las aplican bien con una instrucción simple. Con Verus probaron propiedades irrelevantes y tautologías equivalentes a A ⇒ A. Una skill diseñada para sacarlos del comportamiento por defecto sí funcionó razonablemente; las que recomendó codex, peor que la media.

¿El mal uso de estas técnicas es solo un problema de Zstd?

No. Luu no vio diferencias materiales en el eval del RFC de IMAP, 40 ejecuciones por condición, ni en otros RFCs. El mal uso se repite en problemas de protocolo, no solo en manipulación de bits. En xhigh los agentes pasaban los tests que ellos escribían, pero esos tests eran pobres y no cazaban bugs reales.