Resumo Técnico: Programação de "Vibe" Guiada por Métodos Formais via Engenharia Orientada a Modelos

1. Declaração do Problema

O artigo aborda a lacuna crítica entre a rápida adoção da "programação de vibe" (vibe coding) — um fluxo de trabalho onde desenvolvedores descrevem a intenção em linguagem natural para Grandes Modelos de Linguagem (LLMs) e aceitam o código gerado com revisão mínima — e os requisitos rigorosos de garantia para sistemas críticos de segurança (regidos por normas como DO-178C, IEC 61508 e ISO 26262).

As abordagens atuais para verificar o código gerado por LLMs enfrentam duas barreiras estruturais primárias:

1. Linguagens de Verificação-Conscientes: Métodos direcionados a linguagens como Dafny, Verus ou Lean sofrem com a escassez de dados de pré-treinamento para LLMs, capacidades de raciocínio composicional deficientes e falta de integração com as cadeias de ferramentas industriais existentes (que predominantemente utilizam Java, C ou C++).
2. Filtragem Post-Hoc: Ferramentas existentes que adicionam camadas de verificação após a geração tratam a verificação como um filtro, em vez de um sinal de feedback, não oferecendo nenhum mecanismo para guiar o LLM em direção à correção.

Consequentemente, a programação de vibe não guiada produz artefatos que carecem das garantias de correção formal e das evidências rastreáveis exigidas para certificação.

2. Metodologia: O Pipeline Forge

Os autores apresentam o Forge (Formal method Oriented Refinement loop for GEnerated code), um pipeline de ciclo fechado que integra a geração por LLM com uma infraestrutura estabelecida de Engenharia Orientada a Modelos (MDE). A filosofia central é tratar o LLM como um "gerador de rascunhos" e a cadeia MDE como um "discriminador", permitindo que os desenvolvedores trabalhem em Java convencional enquanto a verificação formal opera sobre modelos extraídos que eles não precisam sequer visualizar.

O pipeline consiste em sete fases agrupadas em três famílias:

Fase 1: Elicitação de Requisitos

Os requisitos em linguagem natural são estruturados em um conjunto de requisitos formais.

Fase 2: Síntese de Código Top-Down (Programação de Vibe)

Um LLM (especificamente o Anthropic Claude Code) gera código-fonte Java baseado em uma sequência de cinco camadas de prompts:

1. Arquitetura: Estrutura de pacotes/classes e mapeamento de requisito-para-classe.
2. Esqueleto: Java compilável com métodos stubbed.
3. Folhas (Leaves): Lógica de sensores, atuadores e operações.
4. Controlador: A lógica da máquina de estados aninhada por modos.
5. Revisão: Autorrelato de valores padrão inventados.

Restrições: Para garantir uma extração de modelo fiel, o LLM é restrito a um subconjunto específico de Java (ex: sem lambdas, streams ou pattern matching; máquinas de estado devem usar estruturas if-else de dois níveis). Este subconjunto é motivado pela tratabilidade da extração de modelos, não pela previsibilidade em tempo de execução.

Verificações de Pré-voo (2a–2c): O código gerado passa por compilação, verificações de cobertura de requisito-para-código e linting estrutural contra as regras de extração.

Fases 3–5: Extração e Transformação

Esta fase converte o código-fonte Java em artefatos formais sem intervenção humana:

• Fase 3 (Texto-para-Modelo): Uma ponte customizada Spoon-to-EMF analisa a AST do Java (suportando recursos do Java 17+ como interfaces seladas e records) em um modelo do Eclipse Modeling Framework (EMF).
• Fase 4 (Modelo-para-Modelo): Um script de Linguagem de Transformação Epsilon (ETL) transforma o modelo EMF do Java em uma máquina de estados RoboChart, identificando modos, transições e guardas.
• Fase 5 (Modelo-para-Texto): Três artefatos formais independentes são gerados:
  1. Especificações Dafny: Geradas diretamente do modelo EMF Java para verificação dedutiva.
  2. Scripts CSP-M: Gerados do modelo RoboChart para verificação de refinamento comportamental.
  3. Teorias Isabelle/HOL: Geradas do modelo RoboChart usando notação Z-Machine para prova de teoremas.

Fases 6–7: Verificação e Refinamento de Ciclo Fechado

• Fase 6 (Verificação): Os três artefatos são verificados por suas respectivas ferramentas:
  • Dafny (Z3): Verifica contratos de função (pré-condições, pós-condições, terminação).
  • FDR4: Verifica propriedades comportamentais (ausência de deadlock, ausência de divergência) via refinamento CSP.
  • Isabelle/HOL: Prova invariantes estruturais e ausência de deadlock sobre a relação de transição simbólica.
  • Auditoria de Vacuidade (6d): Garante que as provas não sejam triviais (ex: não apenas true ou True).
• Fase 7 (Refinamento): Falhas de verificação são traduzidas em prompts de correção estruturados e acionáveis (JSON/Markdown). Esses prompts, vinculados a requisitos específicos e linhas de código fonte via uma cadeia de rastreabilidade, são enviados de volta ao LLM para regenerar o código. O ciclo continua até que todos os verificadores passem ou um número máximo de iterações seja atingido.

3. Principais Contribuições

1. Ciclo Fechado de Rascunho-e-Discriminação: Uma arquitetura inovadora onde o código em linguagem comum gerado por LLM torna-se formalmente verificável ao ser roteado através de infraestrutura MDE, utilizando falhas de verificação como sinais de correção iterativa em vez de filtros post-hoc.
2. Ponte Spoon-to-EMF: A primeira transformação texto-para-modelo nativa de EMF para Java moderno (17+), capaz de lidar com interfaces seladas, records e sintaxe de pattern, preenchendo uma lacuna deixada por ferramentas legadas como o MoDisco.
3. Design de Três Verificadores Complementares: Um sistema que emprega Dafny, FDR4 e Isabelle/HOL em paralelo. O artigo demonstra que esses verificadores não são intercambiáveis; cada um detecta classes distintas de defeitos (ex: Dafny detecta violações de contrato, FDR4 detecta deadlocks comportamentais, Isabelle detecta deadlocks estruturais).
4. Rastreabilidade de Ponta a Ponta: Uma cadeia totalmente rastreável que liga requisitos em linguagem natural através do código gerado, modelos intermediários e provas formais, permitindo diretrizes de correção por requisito.
5. Validação Empírica: Evidência de que o loop converge para código totalmente verificado em múltiplos experimentos independentes, impulsionado especificamente pelo feedback do verificador.

4. Resultados Experimentais

O pipeline foi avaliado em três estudos de caso de autoria externa com complexidade crescente:

• SRanger: Um robô terrestre de controlador único (23 requisitos, ~220 LOC).
• Last Response Engine (LRE): Um governador de segurança de um AUV (51 requisitos, ~613 LOC).
• Chemical Detector: Um robô autônomo de múltiplos controladores (81 requisitos, ~618 LOC).

Principais Descobertas:

• Convergência: Em 15 execuções independentes (5 por estudo de caso), todas as 15 execuções convergiram para código totalmente verificado dentro de 2 a 3 iterações (mediana 2).
• Necessidade de Feedback: Em um experimento de "linha de base fria" (30 execuções sem feedback do verificador), 0 execuções convergiram. A geração de passagem única falhou em produzir código verificado.
• Papel dos Verificadores: Uma ablação de "apenas compilação" (onde o feedback do verificador era ocultado, mas as verificações de compilação permaneciam) mostrou que todas as 15 execuções ainda produziram artefatos que falharam em pelo menos um verificador formal. Isso confirma que o feedback do verificador, e não apenas a iteração ou compilação, impulsiona a convergência.
• Detecção de Defeitos: Os três verificadores detectaram defeitos distintos. Por exemplo, um deadlock estrutural em um modo terminal foi perdido pelo Dafny e FDR4, mas capturado pelo Isabelle, exigindo uma correção específica (adição de um laço de auto-permanência idle).
• Custo: A convergência normalmente levou de 2 a 3 iterações. O tempo de execução variou de ~1 a 15 minutos por execução, dominado pelos tempos de prova do Isabelle quando existiam questões estruturais.

5. Significância e Alegações

O artigo afirma demonstrar um argumento estrutural sobre onde a verificação formal deve residir em um fluxo de trabalho orientado por LLM: não dentro do LLM, e não como um filtro post-hoc, mas como o discriminador em um processo de refinamento de ciclo fechado.

• Relevância para Certificação: O pipeline produz tipos de evidência reconhecidos por normas de segurança (verificação dedutiva, verificação de refinamento e prova de teoremas), oferecendo um caminho para a certificação de código gerado por IA sem exigir que engenheiros aprendam linguagens formais ou abandonem suas cadeias de ferramentas Java existentes.
• Viabilidade: Prova que o código gerado por LLM em linguagens comuns pode ser sistematicamente transformado em modelos formais e verificado, desde que haja uma robusta pipeline de extração e transformação em vigor.
• Modéstia: Os autores declaram explicitamente que este trabalho fornece evidências para um caso de certificação, não a certificação em si. Eles reconhecem que a certificação total exigiria etapas adicionais, incluindo qualificação de ferramentas, evidências de processo e revisão independente do caso de garantia, que permanecem como trabalhos futuros. A contribuição é a existência de um pipeline viável que fecha o ciclo de verificação.