Los modelos de lenguaje grande (LLMs) están facilitando el uso de TLA+ (Temporal Logic of Actions), un lenguaje de verificación formal inventedo por Leslie Lamport en la década de 1990. Según el ingeniero Jesse Jiryu Davis en un artículo publicado en emptysqua.re, los LLMs Frontier pueden generar código TLA+ fácilmente, superando una de las principales barreras históricas: la sintaxis hostil que imitate LaTeX. El artículo presenta un problema de ejemplo consistente en un recipiente con judías blancas y negras, donde el algoritmo elimina dos judías del mismo color y añade una blanca, o elimina dos de colores diferentes y añade una negra. Davis explica que al escribir este problema en TLA+, un verificador de modelos puede responder automáticamente si el algoritmo puede terminar con cero judías o con una sola. Aunque los LLMs facilitan la generación de código, Davis advierte que sigue siendo responsabilidad del ingeniero comprender su sistema y definir qué significa "corrección", además de requerir un entendimiento alto de lógica temporal. El artículo incluye un ejemplo de prompt para iniciar una especificación TLA+ con el LLM Claude.
Los LLMs hacen accesible la verificación formal con TLA+
