Métodos formales y el futuro de la programación: qué vale la pena probar y dónde está el techo

Hay una conversación que se repite en ciclos de tres o cuatro años. Alguien publica que los formal methods —verificación formal, especificación matemática, model checking— son la respuesta a los bugs que seguimos cometiendo después de décadas de avance en herramientas. El hilo de HN se llena de comentarios de personas que usaron TLA+ en sistemas distribuidos, de otras que intentaron Alloy en un proyecto real y lo abandonaron a la segunda semana, y de unas pocas que dicen que en AWS o en Microsoft ya corren esto en producción hace años.

El problema no es que la conversación sea falsa. El problema es que, cada vez que la leo, siento que está incompleta de la misma manera: habla del potencial sin hablar del costo de instalación, de los prerrequisitos de equipo y de los casos donde la verificación formal no escala —no conceptualmente, sino operativamente, en un equipo de cinco personas con un deadline real.

Mi tesis concreta: los formal methods señalan un problema genuino que TypeScript, tests y linters no resuelven del todo. Pero convertir eso en una decisión técnica requiere saber exactamente qué compra cada herramienta y a qué precio. Repetir "deberíamos usarlo" sin esa matriz no es criterio técnico, es hype con mejor vocabulario.

El problema real que señalan los formal methods

Antes de hablar de herramientas, vale la pena nombrar qué falla en el flujo actual.

Cuando diseñamos un sistema con TypeScript y Zod —como hice al pensar en validación de runtime en producción— ganamos una cosa muy concreta: si el tipo dice string, en runtime también es string. Eso elimina una clase entera de bugs. Pero no elimina bugs de lógica. Un schema puede ser válido y aun así representar un estado imposible del dominio.

Ejemplo brutal: un sistema de autorizaciones donde role: "admin" y permissions: [] son ambos valores válidos por separado pero juntos no tienen sentido. Zod no te va a decir nada. TypeScript tampoco. El test que escribiste quizás tampoco, porque lo escribiste asumiendo que ese estado no existe.

Eso es exactamente lo que la verificación formal ataca: la demostración de que ciertos estados son imposibles en el espacio completo de ejecuciones posibles del sistema, no solo en los casos que vos tuviste la imaginación de cubrir con tests.

El problema real no es que nos falten herramientas de tipado. Es que los tipos describen la forma de los datos pero raramente capturan las invariantes del negocio. Esa brecha es donde viven los bugs más costosos —los que aparecen en producción después de tres años cuando se da una combinación de eventos que nadie anticipó.

Qué compra cada herramienta y a qué precio

No existe "formal methods" como herramienta única. Es una familia. Vale la pena separar:

TLA+ — Model checking para sistemas distribuidos

TLA+ (desarrollado por Leslie Lamport, documentación pública en lamport.azurewebsites.net) permite especificar el comportamiento de un sistema como un conjunto de estados y transiciones, y luego verificar propiedades sobre todos los estados alcanzables.

AWS lo usa para verificar protocolos distribuidos internos. Eso está documentado en su paper público "Use of Formal Methods at Amazon Web Services" (2014). El dato relevante: lo usan ingenieros que dedican tiempo específico a escribir specs, no como actividad paralela al desarrollo normal.

Lo que compra: encontrar race conditions y violaciones de invariantes en sistemas distribuidos antes de que lleguen a código.

El precio: curva de aprendizaje alta. La sintaxis es no trivial. Escribir una spec correcta requiere pensar el sistema de forma diferente a como pensás cuando escribís código. No es una tarde, es semanas.

Alloy — Especificación ligera para modelos de datos

Alloy (MIT, alloytools.org) es más accesible que TLA+. Permite modelar relaciones entre entidades y verificar propiedades sobre esos modelos. Funciona bien para validar esquemas de autorización, modelos de datos y protocolos simples.

-- Ejemplo: modelo de permisos que detecta estados imposibles
sig User {}
sig Role { permissions: set Permission }
sig Permission {}

-- Invariante: ningún admin puede tener permisos vacíos
fact AdminConstraint {
  all u: User, r: Role |
    r.permissions = none implies r not in AdminRole
}

Lo que compra: detectar contradicciones en el modelo antes de escribir una línea de código de producción.

El precio: el modelo no es el código. Mantener ambos sincronizados es trabajo real. Si el equipo no adopta la práctica, el modelo envejece y se vuelve deuda.

Dafny / F* — Verificación integrada en el código

Dafny (github.com/dafny-lang/dafny) y F* (fstar-lang.org) llevan la verificación al nivel del código mismo: escribís precondiciones, postcondiciones e invariantes como anotaciones, y el verificador prueba que el código las satisface.

// Ejemplo en Dafny: función con precondición verificable
method Divide(a: int, b: int) returns (result: int)
  requires b != 0  // precondición: el verificador garantiza que esto se cumple
  ensures result * b == a  // postcondición verificada formalmente
{
  result := a / b;
}

Lo que compra: garantías más fuertes que los tipos. El verificador rechaza el código si no puede probar las postcondiciones.

El precio: escribir las especificaciones lleva tiempo proporcional a la complejidad del dominio. Para lógica de negocio rica, podés pasar más tiempo en las specs que en el código.

Donde se equivoca la gente

Error 1: tratar los formal methods como reemplazo de tests

Los tests verifican comportamiento en casos específicos. Los formal methods verifican propiedades sobre espacios de estados. Son complementarios, no alternativos. Abandonar tests porque "ahora tengo verificación formal" es como sacar los extintores porque el edificio tiene detector de humo.

Error 2: adoptar la herramienta sin adoptar la práctica

El mayor costo oculto no es el tiempo de aprendizaje inicial. Es el mantenimiento. Una spec TLA+ que no se actualiza cuando cambia el sistema es activamente peligrosa: da falsa confianza. El mismo problema que con los tests que nunca fallan porque ya no testean el código real.

Error 3: aplicarlo a todo el sistema en lugar de a las invariantes críticas

No necesitás verificar formalmente el endpoint que devuelve el listado de posts. Sí puede tener sentido verificar el protocolo de autenticación, el sistema de permisos o el mecanismo de reintento con idempotencia. La pregunta correcta no es "¿debería usar formal methods?" sino "¿qué invariante de mi sistema, si se viola, es catastrófica y no tengo cómo probarla con tests?". Algo parecido aplica cuando diseñás tokens de autenticación con semántica de expiración: la lógica de cuándo un token es válido tiene exactamente esa forma —estados que parecen correctos por separado pero pueden ser inválidos en combinación.

Error 4: subestimar el prerequisito de abstracción

Para usar TLA+ o Alloy necesitás poder pensar el sistema como un modelo abstracto. Eso no es habilidad universal. En equipos donde la mayoría de las personas trabaja pegadas al framework —lo cual no es una crítica, es una realidad operativa— introducir formal methods sin preparación es una inversión que no retorna.

Matriz de decisión: cuándo vale la pena y cuándo no

Antes de decidir si explorar alguna de estas herramientas, pasá por esta lista:

CHECKLIST: ¿Formal methods tiene sentido aquí?

Señales de que SÍ vale explorar:
  [ ] El sistema tiene invariantes de negocio críticas que los tests no cubren exhaustivamente
  [ ] Ya tuviste un bug en producción causado por un estado que "no debería existir"
  [ ] El dominio tiene lógica de autorización, transacciones o estados distribuidos complejos
  [ ] El equipo tiene al menos una persona dispuesta a invertir 2-4 semanas en aprendizaje inicial
  [ ] Hay presupuesto de tiempo para mantener las specs actualizadas

Señales de que NO es el momento:
  [ ] El equipo está por debajo de cobertura de tests básica
  [ ] No hay documentación actualizada del dominio
  [ ] El roadmap tiene features nuevas cada sprint sin tiempo de consolidación
  [ ] Nadie puede articular qué invariante específica querés verificar
  [ ] El problema principal es velocidad de entrega, no corrección de propiedades

Para un stack Next.js + TypeScript + PostgreSQL como el mío: el caso más plausible de entrada no es TLA+ para distribuidos —no tenés ese nivel de concurrencia por defecto. Es Alloy para modelar el sistema de permisos o de estados de una entidad antes de escribir las migraciones. Eso sí es costo/beneficio razonable: un par de horas de modelado que pueden evitar una migración de datos costosa después.

Cuando diseñé el sistema de caching en Next.js App Router, el problema de fondo era exactamente ese: estados de cache que parecían válidos individualmente pero eran inconsistentes en combinación. Un modelo Alloy básico del ciclo revalidate → stale → fresh hubiese hecho el problema más visible antes de llegar al código.

FAQ

¿Formal methods reemplaza a TypeScript o a Zod?
No. TypeScript y Zod capturan la forma de los datos. Los formal methods capturan invariantes lógicas sobre el comportamiento del sistema. Son capas diferentes. Si ya estás usando validación con Zod en cliente y servidor, los formal methods serían el paso siguiente para las invariantes que Zod no puede expresar.

¿TLA+ se usa en producción real o es solo académico?
AWS y Microsoft Research tienen papers públicos documentando el uso de TLA+ en sistemas internos. Intel usó model checking para verificar hardware. No es solo académico, pero tampoco es mayoritario en la industria general. La adopción está concentrada en sistemas críticos donde el costo de un bug es muy alto.

¿Cuánto tiempo lleva aprender TLA+ a un nivel útil?
Dependiendo de la base matemática y la experiencia con sistemas distribuidos, la estimación razonable que aparece en la documentación oficial y en los recursos de la comunidad es de 2 a 8 semanas para escribir specs básicas útiles. No es un fin de semana.

¿Vale la pena para un proyecto personal o indie?
Depende del dominio. Si estás construyendo un sistema de pagos, autorización o sincronización de datos con semántica compleja, modelar las invariantes con Alloy antes de escribir el schema puede ahorrarte horas. Si estás construyendo un blog o un CRUD estándar, es overkill.

¿Qué pasa con los MCP tools o agentes de IA? ¿Aplica ahí?
Más de lo que parece. Los MCP tools portables tienen exactamente el problema de invariantes de estado: qué herramientas pueden llamarse en qué orden, qué precondiciones necesita cada tool, qué garantiza cada resultado. Es un caso donde modelar el protocolo con Alloy antes de implementar tiene sentido concreto.

¿Los formal methods sirven para sistemas con bases de datos como PostgreSQL?
Para el protocolo de acceso y las invariantes de consistencia, sí. Para queries individuales, no —ahí Prisma y los logs son más útiles, como vimos en el análisis de Prisma query logging. La frontera es: si la pregunta es "¿este estado es posible?", formal methods. Si la pregunta es "¿qué tan rápido va esta query?", observabilidad y explain.

Cerrando: mi postura después de 30 años mirando esto

Los formal methods no van a reemplazar el oficio de escribir software. Lo que sí hacen, cuando se usan con criterio, es forzar una pregunta que la mayoría de los equipos evita hasta que es tarde: ¿qué estados de este sistema son imposibles y cómo lo sabemos?

Lo que no compro es la narrativa de que la industria los ignoró por ignorancia o por flojera. Los ignoró porque el costo de adopción es alto y los beneficios son difíciles de medir antes de que algo falle. Eso no es irracionalidad, es una decisión de trade-off con consecuencias que recién se ven en el largo plazo.

Mi recomendación práctica para alguien con un stack moderno: antes de TLA+ o Dafny, empezá con Alloy para modelar el dominio más crítico del sistema. Una tarde. Sin presión de adopción completa. Si en esa tarde encontrás un estado que no habías visto, el experimento valió. Si no encontrás nada nuevo, lo usaste para validar que el modelo mental del equipo era correcto. Ambos resultados tienen valor.

Lo que no hagas es leer el thread de HN, sentir que deberías estar usando TLA+ y agregarlo al backlog sin una invariante concreta que querés verificar. Eso es hype disfrazado de disciplina técnica. Y después de 30 años viendo ciclos de esto, esa es la distinción que más vale sostener.

¿Tenés una invariante de negocio en el sistema en el que estás trabajando que los tests no cubren exhaustivamente? Ese es el lugar concreto donde empezar a mirar.

Este artículo fue publicado originalmente en juanchi.dev