La semana pasada, Boris Cherny, el inventor de Claude Code, mencionó que Opus pudo usar TLA+ para encontrar condiciones de carrera en el código. Ahora todo el mundo habla de verificación formal. Como educador y defensor de TLA+ desde hace mucho tiempo, esto es emocionante. Pero la nueva euforia me preocupa. Los métodos formales no resolverán el desarrollo de software agente de una vez por todas.

Los diseños correctos no se traducen automáticamente en código correcto. Para verificar una propiedad, necesitamos una propiedad que verificar. TLA+ divide el sistema en comportamientos, cada uno una secuencia de estados. En cada estado podemos expresar expresiones booleanas con tres operadores temporales: `[]P` (siempre P), `P'` (P en el siguiente estado) y `<>P` (eventualmente P).

`[]P` significa que P es verdadero en cada estado de cada comportamiento, llamado invariante. `[](x' >= x)` es una propiedad de acción. Estas son propiedades de seguridad: algo malo nunca sucede. Las propiedades de vivacidad usan `<>`: `[]<>P` significa que P es verdadero en al menos un estado futuro de cada estado; `<>[]P` significa que P se vuelve verdadero y permanece verdadero para siempre; `[](P => <>Q)` significa que P eventualmente causa Q.