Agentes LLM y la Verificación Formal de Compiladores: Un Deep Dive en la Construcción de un Compilador JS-to-WASM Ver...

La verificación formal de software, que utiliza pruebas matemáticas para asegurar la corrección del código, ha sido históricamente un proceso intensivo en mano de obra experta. Con el auge de los modelos de lenguaje grandes (LLM) y la ingeniería de software asistida por agentes, surge la pregunta de si estas herramientas pueden automatizar o acelerar la creación de software verificado. Este experimento aborda un problema fundamental de la computación: la construcción de un compilador que no solo traduce código de un lenguaje a otro, sino que también garantiza matemáticamente que la semántica del programa se preserva durante la traducción. La relevancia de este desafío se amplifica en la era del código generado por IA, donde la fiabilidad y la seguridad son preocupaciones primordiales.

El problema de la verificación de compiladores no es nuevo; se remonta a la propuesta de Tony Hoare en 2003 de un "compilador verificador" como un gran desafío para la computación. Proyectos como CompCert y seL4 han demostrado la viabilidad de la verificación formal para sistemas críticos, pero a un costo humano considerable. El experimento busca determinar si los agentes LLM pueden cerrar la brecha entre la generación de código funcional (que pasa pruebas) y la generación de código formalmente correcto (matemáticamente probado), un paso crucial para escalar la confianza en sistemas complejos y generados automáticamente.

Arquitectura del Sistema

El sistema se basa en un pipeline de compilación de JavaScript a WebAssembly, con la particularidad de que cada componente y la traducción entre ellos deben ser formalmente verificados. La arquitectura conceptual se articula en torno a cuatro artefactos clave: una semántica formal para el lenguaje fuente (JavaScript), una semántica formal para el lenguaje objetivo (WebAssembly), el compilador en sí mismo (que traduce JS a WASM a través de varias fases intermedias), y una prueba matemática que demuestra que la traducción preserva el significado del programa. Este último es el corazón de la verificación.

La implementación se realizó en Lean 4, un asistente de pruebas y lenguaje de programación funcional. Los agentes LLM (Claude Code) fueron desplegados en una configuración multi-agente: tres agentes "worker" (uno para la especificación JS, otro para la especificación WASM y un tercero para la escritura de pruebas del compilador) y un agente "supervisor" encargado de la coordinación y la resolución de bloqueos. La comunicación entre agentes se gestionó mediante permisos de sistema de archivos Unix y el supervisor reescribía los prompts de los workers. El pipeline de compilación incluye fases como JS → Core, Core → Flat, Flat → ANF y ANF → WASM. Cada fase requiere su propia "relación de simulación" (simulation relation), un invariante preciso que describe cómo los estados del lenguaje fuente y objetivo se corresponden en cada paso de la ejecución. La verificación de estas relaciones es crucial para la prueba de corrección general del compilador. Conceptos como partial def en Lean, termination_by, decreasing_by y el uso de simp para la simplificación de pruebas son centrales en el proceso de verificación.

inductive Expr where | num : Int → Expr | add : Expr → Expr → Expr
def eval_js : Expr → Int | .num n => n | .add a b => eval_js a + eval_js b
def compile : Expr → WasmExpr | .num n => .i32_const n | .add a b => .i32_add (compile a) (compile b)
theorem correctness (e : Expr) : eval_wasm (compile e) = eval_js e := by induction e with | num n => simp [compile, eval_js, eval_wasm] | add a b ih_a ih_b => simp [compile, eval_js, eval_wasm, ih_a, ih_b]

def HeapCorr (cheap fheap : Core.Heap) : Prop := cheap.objects.size ≤ fheap.objects.size ∧ ∀ addr, addr < cheap.objects.size → cheap.objects[addr]? = fheap.objects[addr]?

Fundamentos Teóricos

El concepto de un compilador verificador se basa en los fundamentos de la semántica formal de los lenguajes de programación y la lógica matemática. La idea de que un compilador debe preservar el significado de un programa se formaliza a través de la noción de "correctness by construction" o "semantic preservation". Esto se remonta a trabajos pioneros en la teoría de compiladores y la verificación formal, como el artículo de Robin Milner "A Calculus of Communicating Systems" (1980) que sentó las bases para la semántica operacional, o el trabajo de John McCarthy en la década de 1960 sobre la verificación de programas.

El "diagrama conmutativo" que describe la propiedad de corrección de un compilador es una representación estándar en la teoría de compiladores verificados, popularizada por proyectos como CompCert (Leroy, 2009). Este diagrama establece que la evaluación de un programa fuente y la posterior compilación debe ser equivalente a la compilación del programa fuente y su posterior evaluación. La dificultad radica en formalizar las semánticas de los lenguajes (eval_js, eval_wasm) y la función de compilación (compile) de manera que se pueda construir una prueba mecánica de esta equivalencia. El proceso de refinamiento iterativo de las relaciones de simulación, similar al "Counterexample-Guided Inductive Synthesis" (CEGIS) o "Counterexample-Guided Abstraction Refinement" (CEGAR), es una técnica bien establecida en la verificación formal y la síntesis de programas, donde los fallos en la prueba o la ejecución se utilizan para refinar las especificaciones o las abstracciones.