Anthropic publicó el 22 de octubre de 2026 un trabajo de su Frontier Red Team con un título que va directo al grano: los modelos de lenguaje están haciendo viable la verificación formal de software a una escala mucho mayor. Dos días antes, el 20, el mismo equipo había sacado otro sobre usar Claude para reducir la superficie de ataque del código. Algún medio lo ha resumido como «Claude escribe el código y demuestra que es seguro, solo». Ese resumen se pasa de frenada, pero debajo hay algo que sí me parece de las cosas más serias que han salido este año.
Qué ha pasado
La página del Frontier Red Team lleva 34 publicaciones y, si bajas por el listado, el último año se lee casi como un informe de capacidades ofensivas y defensivas en paralelo: en diciembre de 2025, agentes encontrando 4,6 millones de dólares en fallos explotables de contratos inteligentes; en enero de 2026, búsqueda de bugs por el ecosistema Python con pruebas basadas en propiedades; el 8 de octubre, el escáner opt-in para código abierto; el 29 de septiembre, un aviso sobre GLM-5.3 y la difusión de capacidades ciber avanzadas sin salvaguardas.
Y ahora, estas dos últimas entradas, que van de lo contrario: usar la misma capacidad para cerrar agujeros en vez de abrirlos. El detalle técnico está en su publicación —yo te enlazo el índice del equipo para que lo leas de primera mano, no me lo creas a mí—, pero la tesis es la del titular: lo que antes solo se podía hacer en tres o cuatro proyectos del mundo, ahora cabe en más sitios.
Por qué importa
Verificación formal significa demostrar matemáticamente que un trozo de código cumple una especificación. No «he pasado 400 tests y no ha petado», sino «no existe ninguna entrada que lo rompa, y aquí está la prueba». Se hace con lenguajes como Lean o Dafny, y el resultado lo comprueba una máquina, no un revisor con sueño.
El problema nunca fue la idea. Fue el coste. Escribir la demostración de una función cuesta mucho más que escribir la función: hay que dar con los invariantes, pelearse con el asistente de pruebas, repetir. Por eso la verificación formal vive en microkernels, compiladores y poco más. El resto del mundo escribe tests y reza.
Ahí es donde entra el modelo, y la razón por la que esto funciona no es que Claude sea muy listo. Es que hay un verificador determinista al final del tubo. El modelo puede generar cien intentos de demostración, noventa y nueve basura, y da igual: el comprobador los rechaza sin discutir. No hay alucinación que sobreviva a un juez que responde sí o no. Es el mismo patrón que hace que los modelos sean buenos compilando, corrigiendo tests o haciendo fuzzing, y malos escribiendo el informe anual: cuando existe un oráculo barato, la fuerza bruta del modelo se convierte en resultado.
Qué haría distinto alguien a partir de hoy. No verificar la aplicación entera —eso sigue sin tener sentido—, sino elegir las tres o cuatro funciones que no te puedes permitir que fallen y meterles una especificación de verdad. El parser que come datos de fuera. El cálculo de importes con redondeo. La máquina de estados de la autenticación. La parte de concurrencia que nadie toca desde 2021 porque da miedo. Son trozos pequeños, muy caros si fallan, e imposibles de cubrir con tests exhaustivos.
Qué no cambia
Y ahora la letra pequeña, que aquí es grande.
- Una demostración solo prueba lo que dice la especificación. Si la especificación está mal, tienes un código perfectamente correcto haciendo lo que no querías. El bug no desaparece: se muda río arriba, a un sitio donde hay menos gente mirando.
- La base de confianza sigue ahí: el compilador, el propio comprobador de pruebas, el hardware, y toda frontera donde tu código verificado llama a código que no lo está. Normalmente esa frontera es enorme.
- No te cubre nada de lo que de verdad te tumba un martes: la dependencia con un mantenedor nuevo, el bucket abierto, el secreto en los logs, la copia de seguridad que nunca se restauró.
- «Automáticamente» es del titular, no del paper. Lo que dicen es que ahora es viable a mayor escala. Hay distancia entre eso y «ya está resuelto», y conviene no acortarla por nosotros.
- Y una incómoda: la capacidad que escribe demostraciones es la misma que escribe exploits. El mismo equipo publica las dos cosas, y eso no es contradicción, es el mapa real.
Nuestra lectura
A mí esto me parece, de largo, lo más interesante que ha pasado este año en IA aplicada a código. Más que los agentes que te escriben un CRUD en veinte minutos. Y la razón es exactamente la que decía arriba: el oráculo.
Llevo tiempo con la misma regla y esto la refuerza. Donde hay un comprobador barato y determinista, los modelos rinden de forma absurda. Donde el único juez es un humano leyendo un diff el viernes a las siete, es una lotería. Todo el esfuerzo útil de los próximos dos años no está en modelos más grandes: está en fabricar oráculos para sitios donde hoy no los hay. La verificación formal es el caso extremo y por eso se nota tanto.
Lo que creo que va a envejecer mal: la palabra «verificado». Doy año y medio para que aparezca en una landing como sello, y dos para que alguien venda «verificado por IA» queriendo decir que el modelo lo miró y le pareció bien. Cuando lo veas, pregunta tres cosas: qué especificación, qué comprobador y qué versión, y qué queda fuera de la frontera verificada. Si no hay respuesta a las tres, es marketing.
Y un consejo poco glamuroso: antes de montar Lean en tu proyecto, mira si te falta algo más básico. En la mayoría de los códigos que me llegan, las pruebas basadas en propiedades —generar miles de entradas al azar y comprobar que se cumple una regla— te dan el ochenta por ciento del valor por una fracción del esfuerzo. El propio equipo de Anthropic lleva un año usando ese camino para encontrar bugs. Empieza por ahí.
Esto es justo lo que nos encontramos cuando alguien nos pide meter IA en su desarrollo: la pregunta buena no es cuánto código más puede escribir el modelo, sino qué red automática hay debajo para decir que ese código está bien sin que nadie tenga que opinar. Cuando esa red no existe, generar más rápido solo sirve para acumular deuda antes.
Cualquier duda me dices y lo vemos. Un saludo, Vicente.