TLA+ no verifica todo lo que se le atribuye: los límites que nadie menciona
El auge de la verificación formal tras el hallazgo de Opus con TLA+ choca con sus límites reales: propiedades de alcance, hiperpropiedades y tiempo real quedan fuera.
Boris Cherny, el creador de Claude Code, comentó la semana pasada que Opus había sido capaz de usar TLA+ para localizar condiciones de carrera en código. A partir de ahí, media internet se ha puesto a hablar de verificación formal como si fuera la pieza que faltaba. Hillel Wayne, que lleva años enseñando y divulgando TLA+, pone el freno: hay familias enteras de propiedades que la herramienta ni siquiera puede expresar, y por tanto nunca podrá comprobar.
El aviso no va contra TLA+. Wayne es de los primeros interesados en que se use, y defiende que sirve para diseñar sistemas concurrentes complejos sin errores. Lo que le preocupa es el salto que se está dando desde "un modelo encontró una condición de carrera" hasta "los métodos formales resuelven el desarrollo agéntico de una vez por todas".
Qué sí entra
TLA+ parte el sistema en comportamientos, y cada comportamiento es una secuencia de estados. Sobre esos estados se escriben expresiones booleanas y se aplican tres operadores temporales: []P (P siempre), P' (P en el estado siguiente) y <>P (P en algún momento). Con eso salen los invariantes, las propiedades de acción como [](x' >= x) y la vivacidad: []<>P para mecanismos de recuperación, <>[]P para demostrar que un algoritmo termina con el resultado correcto, o [](P => <>Q), que se escribe P ~> Q, para decir que una cosa acaba provocando otra. La mayoría de lo que se comprueba en la práctica son invariantes, propiedades de acción y vivacidad, más el refinamiento.
Si vienes de cero, la propia comunidad mantiene material para aprender TLA+, y Wayne tiene un artículo aparte explicando la diferencia entre seguridad y vivacidad.
El borde del mapa
El primer límite es el más obvio: si no sabes convertir tu propiedad en una fórmula lógica, ninguna herramienta te salva. Si no puedes formalizar la idea humana de pájaro, no vas a demostrar que tu aplicación reconoce pájaros. Muchas de las propiedades que de verdad importan caen ahí.
El segundo son las propiedades demasiado concretas. Los invariantes viven en un estado y las propiedades de acción en una única transición, así que no puedes definir de forma nativa algo como "pulsar borrar y después deshacer devuelve el estado original" o "al pulsar encendido el equipo arranca en menos de diez pasos". Tampoco hay propiedades sobre coma flotante ni sobre tiempo real: el reloj de TLA+ es lógico.
El tercero es el que más le interesa a Wayne. Las propiedades de TLA+ se cuantifican implícitamente sobre todos los comportamientos: lo que se comprueba tiene que ser cierto en cada comportamiento individual. Eso deja fuera la posibilidad, es decir, no se puede afirmar que exista un comportamiento donde P sea alcanzable, algo que haría falta para demostrar que un juego se puede ganar. Y deja fuera las hiperpropiedades, propiedades sobre conjuntos de comportamientos, como probar que el modo de ahorro de energía consume menos que el modo normal en cualquier escenario.
Wayne ya había escrito antes sobre la otra debilidad conocida: un diseño correcto no se traduce solo en código correcto. Ese sigue siendo el hueco por el que se cuela la mayor parte del entusiasmo actual, porque los agentes que escriben código necesitan exactamente eso, que la garantía sobreviva a la generación. Saber dónde están los bordes de la herramienta es lo que permite decidir si merece la pena meterla en el pipeline o quedarse con los tests de siempre.
