Boris Cherny, el que creó Claude Code, publicó el 22 de septiembre que usó Claude Opus 5.5 para verificar formalmente el Claude Agent SDK con Lean. Dos prompts cortos. Dieciséis PRs corrigiendo bugs y condiciones de carrera. Cherny dice que no domina ni Lean ni TLA+. Opus 5.5 sí.

Cuarenta años. Eso es lo que llevan Lean y TLA+ dando vueltas en universidades y en un puñado de equipos de sistemas críticos (Amazon usa TLA+ para AWS, Microsoft y CrowdStrike también, según documenta el propio sitio del lenguaje) sin volverse práctica común. La razón nunca fue que la verificación formal no sirviera. Es que exige pensar en lógica de predicados y en invariantes de estado, no en el lenguaje de programación del día a día. Esa barrera de entrada, la que mantenía los métodos formales fuera de casi cualquier equipo que no fuera de un banco central o una agencia espacial, se está cayendo. Y esta vez no se quedó en promesa de conferencia. Un ingeniero de Anthropic corrigió condiciones de carrera reales en un SDK que ya usan miles de desarrolladores.

Lo que hizo Cherny, sin traducirlo al hype

El post en X es corto y específico: “Usé Opus 5.5 para verificar formalmente el Claude Agent SDK con Lean. Un par de prompts cortos igual a 16 PRs corrigiendo varios bugs y condiciones de carrera. TLA+ también funciona bien. A veces combino Lean y TLA+ para buscar problemas de flujo de datos, concurrencia y manejo de estado. No domino ninguno de los dos lenguajes bien, pero Claude es excelente en ambos.” Video adjunto, que no vi porque no abrí X para esta nota; me quedo con lo que él mismo escribió.

Shreyans Bhansali comentó algo que capta el cambio mejor que cualquier análisis mío: había evitado métodos formales por la curva de aprendizaje, y los agentes básicamente eliminan esa excusa. Kenan W. fue un paso más allá y dijo que esto vuelve los métodos formales lo bastante baratos como para funcionar de capa de gobernanza, no solo de herramienta de un equipo de investigación.

El Claude Agent SDK es el mismo motor que corre Claude Code, empaquetado como librería para que cualquier equipo construya sus propios agentes encima. Corre con concurrencia real, colas y estado compartido entre sesiones. Ahí es donde un bug de condición de carrera se esconde durante meses hasta que un cliente lo encuentra en producción.

La objeción que sí hay que tomarse en serio

En los comentarios de ese mismo post, Mustapha Derzi (VP de desarrollo de aplicaciones, más de 30 años en esto) hizo la pregunta correcta: cuando Claude escribe tanto el modelo en Lean como la prueba, ¿qué detecta el caso en que el modelo se desvía calladamente de lo que el código realmente hace? El bug vive justo ahí, en la brecha entre el modelo y el código.

Maksim Al Dandan le respondió con la precisión que le faltaba a la euforia del hilo: una prueba formal es sobre el modelo, no sobre el código. El spec se convierte en el artefacto que un humano tiene que revisar a mano, y la ventaja real es que el spec es mucho más chico que el código completo. Pero eso no elimina el trabajo de revisión. Lo mueve.

Esto me parece el punto que todos los que celebran esto sin matices se están saltando. Si Claude te escribe 16 PRs a partir de un modelo en Lean que también escribió Claude, alguien en tu equipo tiene que leer ese modelo y confirmar que capturó bien las reglas del sistema real. Sale más barato que leer todo el código concurrente línea por línea buscando la misma carrera de datos. Pero trabajo gratis no es.

Dónde esto vale la pena, y dónde no

Aquí es donde lo llevo a la práctica de ingeniería agéntica que usamos en IQ Source, no a la anécdota de LinkedIn.

Vale la pena modelar en Lean o en TLA+ cuando el sistema tiene concurrencia real: colas de trabajos, locks, reintentos, más de un proceso escribiendo el mismo estado. Vale la pena en máquinas de estado con transiciones que importan, como un flujo de aprobación o un pipeline de facturación. Vale la pena en integraciones entre sistemas donde una orden de pago puede duplicarse o perderse si dos servicios no están de acuerdo en qué pasó primero. En esos tres casos, un test unitario prueba un camino a la vez y un modelo formal busca contraejemplos en todos los caminos posibles.

No vale la pena en un CRUD estándar. No vale la pena en un script que corre una vez y se descarta. Y no vale la pena si nadie en tu equipo va a revisar el spec que Claude escribió, porque entonces solo cambiaste dónde se esconde el bug, no si existe.

La verificación formal no se volvió infalible esta semana. Lo que bajó fue el costo de escribir el primer modelo, lo suficiente para probarlo en un sprint y no en un trimestre. Si tu sistema tiene una máquina de estados o un flujo de concurrencia que te ha mordido antes, ese es el candidato. Empieza ahí, no con todo el codebase.

Nosotros ya integramos revisión de flujos concurrentes y de estado dentro de la auditoría de software, y esto es una herramienta más para esa caja, no un reemplazo del criterio de quien la usa. Lo mismo pasó con la revisión de código cuando el 41% ya lo escribe la IA: el trabajo no desaparece, cambia de forma. Y calza con algo que ya veníamos documentando sobre los cuatro loops que reemplazaron al prompt engineering: cada vez que un agente hace un paso técnico más barato, el paso que sigue siendo caro es el que un humano tiene que aprobar con criterio.