Resumen Técnico: Programación de Sensaciones (Vibe Coding) Guiada por Métodos Formales mediante Ingeniería Dirigida por Modelos

1. Declaración del Problema

El artículo aborda la brecha crítica entre la rápida adopción de la "programación de sensaciones" (vibe coding) —un flujo de trabajo donde los desarrolladores describen la intención en lenguaje natural a Modelos de Lenguaje Extensos (LLM) y aceptan el código generado con una revisión mínima— y los rigurosos requisitos de aseguramiento para sistemas críticos de seguridad (regidos por estándares como DO-178C, IEC 61508 e ISO 26262).

Los enfoques actuales para verificar el código generado por LLM enfrentan dos barreras estructurales primarias:

1. Lenguajes con Conciencia de Verificación: Los métodos dirigidos a lenguajes como Dafny, Verus o Lean sufren de escasez en los datos de preentrenamiento de los LLM, capacidades de razonamiento compositivo deficientes y una falta de integración con las cadenas de herramientas industriales existentes (que predominantemente usan Java, C o C++).
2. Filtrado Post-hoc: Las herramientas existentes que añaden capas de verificación después de la generación tratan la verificación como un filtro en lugar de una señal de retroalimentación, sin ofrecer un mecanismo para guiar al LLM hacia la corrección.

Consecuentemente, la programación de sensaciones no guiada produce artefactos que carecen de las garantías de corrección formal y la evidencia trazable requeridas para la certificación.

2. Metodología: El Pipeline Forge

Los autores presentan Forge (Formal method Oriented Refinement loop for GEnerated code), un pipeline de ciclo cerrado que integra la generación por LLM con infraestructura establecida de Ingeniería Dirigida por Modelos (MDE). La filosofía central es tratar al LLM como un "generador de borradores" y a la cadena MDE como un "discriminador", permitiendo a los desarrolladores trabajar en Java convencional mientras la verificación formal opera sobre modelos extraídos que ellos nunca necesitan ver.

El pipeline consta de siete fases agrupadas en tres familias:

Fase 1: Elicitación de Requisitos

Los requisitos en lenguaje natural se estructuran en un conjunto de requisitos formales.

Fase 2: Síntesis de Código Top-Down (Vibe Coding)

Un LLM (específicamente Anthropic Claude Code) genera código fuente Java basado en una secuencia de cinco capas de prompts:

1. Arquitectura: Estructura de paquetes/clases y mapeo de requisitos a clases.
2. Esqueleto (Skeleton): Java compilable con métodos estipulados (stubs).
3. Hojas (Leaves): Lógica de sensores, actuadores y operaciones.
4. Controlador: La lógica de la máquina de estados anidada por modos.
5. Revisión: Autoinforme de valores por defecto inventados.

Restricciones: Para asegurar una extracción de modelo fiel, el LLM está restringido a un subconjunto específico de Java (por ejemplo, sin lambdas, streams o pattern matching; las máquinas de estados deben usar estructuras if-else de dos niveles). Este subconjunto está motivado por la tractabilidad de la extracción de modelos más que por la predictibilidad en tiempo de ejecución.

Controles de Pre-vuelo (2a–2c): El código generado se somete a compilación, verificaciones de cobertura de requisito-a-código y linting estructural contra las reglas de extracción.

Fases 3–5: Extracción y Transformación

Esta fase convierte el código Java en artefactos formales sin intervención humana:

• Fase 3 (Text-to-Model): Un puente Spoon-to-EMF personalizado analiza el AST de Java (soporta características de Java 17+ como interfaces selladas y records) en un modelo de Eclipse Modeling Framework (EMF).
• Fase 4 (Model-to-Model): Un script de Lenguaje de Transformación Epsilon (ETL) transforma el modelo Java EMF en una máquina de estados RoboChart, identificando modos, transiciones y guardas.
• Fase 5 (Model-to-Text): Se generan tres artefactos formales independientes:
  1. Especificaciones de Dafny: Generadas directamente desde el modelo Java EMF para verificación deductiva.
  2. Scripts CSP-M: Generados desde el modelo RoboChart para la verificación de refinamiento de comportamiento.
  3. Teorías de Isabelle/HOL: Generadas desde el modelo RoboChart utilizando la notación Z-Machine para la demostración de teoremas.

Fases 6–7: Verificación y Refinamiento de Ciclo Cerrado

• Fase 6 (Verificación): Los tres artefactos son verificados por sus respectivas herramientas:
  • Dafny (Z3): Verifica contratos a nivel de función (precondiciones, postcondiciones, terminación).
  • FDR4: Verifica propiedades de comportamiento (ausencia de deadlock, ausencia de divergencia) mediante el refinamiento de CSP.
  • Isabelle/HOL: Demuestra invariantes estructurales y ausencia de deadlock sobre la relación de transición simbólica.
  • Auditoría de Vacuidad (6d): Asegura que las pruebas no sean triviales (por ejemplo, no solo true o True).
• Fase 7 (Refinamiento): Los fallos de verificación se traducen en prompts de corrección estructurados y accionables (JSON/Markdown). Estos prompts, vinculados a requisitos específicos y líneas de código fuente mediante una cadena de trazabilidad, se devuelven al LLM para regenerar el código. El bucle continúa hasta que todos los verificadores pasan o se alcanza un máximo de iteraciones.

3. Contribuciones Clave

1. Bucle de Borrador-y-Discriminación de Ciclo Cerrado: Una arquitectura novedosa donde el código de lenguaje principal generado por LLM se hace formalmente verificable mediante el enrutamiento a través de infraestructura MDE, utilizando los fallos de verificación como señales de corrección iterativas en lugar de filtros post-hoc.
2. Puente Spoon-to-EMF: El primer puente text-to-model nativo de EMF para Java moderno (17+), capaz de manejar interfaces selladas, records y sintaxis de patrones, cerrando una brecha dejada por herramientas heredadas como MoDisco.
3. Diseño de Tres Verificadores Complementarios: Un sistema que emplea Dafny, FDR4 e Isabelle/HOL en paralelo. El artículo demuestra que estos verificadores no son intercambiables; cada uno detecta clases distintas de defectos (por ejemplo, Dafny detecta violaciones de contrato, FDR4 detecta deadlocks de comportamiento, Isabelle detecta deadlocks estructurales).
4. Trazabilidad de Extremo a Extremo: Una cadena totalmente trazable que vincula los requisitos en lenguaje natural a través del código fuente generado, los modelos intermedios y las pruebas formales, permitiendo directivas de corrección por cada requisito.
5. Validación Empírica: Evidencia de que el bucle converge hacia código totalmente verificado a través de múltiples ejecuciones independientes, impulsado específicamente por la retroalimentación del verificador.

4. Resultados Experimentales

El pipeline fue evaluado en tres casos de estudio de autoría externa de complejidad creciente:

• SRanger: Un robot terrestre de un solo controlador (23 requisitos, ~220 LOC).
• Last Response Engine (LRE): Un gobernador de seguridad para un AUV (51 requisitos, ~613 LOC).
• Chemical Detector: Un robot autónomo de múltiples controladores (81 requisitos, ~618 LOC).

Hallazgos Clave:

• Convergencia: A través de 15 ejecuciones independientes (5 por caso de estudio), las 15 ejecuciones convergieron a código totalmente verificado dentro de 2 a 3 iteraciones (mediana de 2).
• Necesidad de Retroalimentación: En un experimento de "línea base fría" (30 ejecuciones sin retroalimentación del verificador), 0 ejecuciones convergieron. La generación de una sola pasada falló en producir código verificado.
• Rol de los Verificadores: En una ablación de "solo compilación" (donde la retroalimentación del verificador se ocultó pero se mantuvieron las comprobaciones de compilación), las 15 ejecuciones produjeron artefactos que fallaron al menos un verificador formal. Esto confirma que la retroalimentación del verificador, y no solo la iteración o la compilación, impulsa la convergencia.
• Detección de Defectos: Los tres verificadores detectaron defectos distintos. Por ejemplo, un deadlock estructural en un modo terminal fue omitido por Dafny y FDR4, pero capturado por Isabelle, requiriendo una corrección específica (añadir un bucle de auto-permanencia en idle).
• Costo: La convergencia típicamente tomó de 2 a 3 iteraciones. El tiempo de reloj de pared varió de ~1 a 15 minutos por ejecución, dominado por los tiempos de prueba de Isabelle cuando existían problemas estructurales.

5. Significado y Reivindicaciones

El artículo afirma demostrar un argumento estructural sobre dónde debe residir la verificación formal en un flujo de trabajo impulsado por LLM: no dentro del LLM, ni como un filtro post-hoc, sino como el discriminador en un proceso de refinamiento de ciclo cerrado.

• Relevancia para la Certificación: El pipeline produce tipos de evidencia reconocidos por estándares de seguridad (verificación deductiva, verificación de refinamiento y demostración de teoremas), ofreciendo un camino hacia la certificación de código generado por IA sin requerir que los ingenieros aprendan lenguajes formales o abandonen sus cadenas de herramientas de Java existentes.
• Factibilidad: Demuestra que el código generado por LLM en lenguajes principales puede transformarse sistemáticamente en modelos formales y verificarse, siempre que exista un pipeline de extracción y transformación robusto.
• Modestia: Los autores declaran explícitamente que este trabajo proporciona evidencia hacia un caso de certificación, no la certificación en sí. Reconocen que la certificación completa requeriría pasos adicionales, incluyendo la calificación de herramientas, evidencia de proceso y revisión independiente del caso de aseguramiento, que siguen siendo trabajo futuro. La contribución es la existencia de un pipeline viable que cierra el bucle de verificación.