A engenharia de software Cleanroom exige que você prove que seu código está correto antes de compilá-lo. Isso soa nobre até você passar três horas escrevendo invariantes de loop para uma função que ordena dez inteiros.

O gargalo não é a prova em si. É o boilerplate. Gerar condições de verificação, anotar loops com invariantes e formatar asserções para Dafny, Why3 ou Z3 é tedioso, propenso a erros e profundamente desagradável. Os LLMs são surpreendentemente bons nessa parte. Eles não são bons nas provas de verdade. Entender a diferença é o que torna a automação útil em vez de perigosa.

Por que Obrigações de Prova Manuais Matam a Velocidade de Desenvolvimento

Em Cleanroom, você escreve código a partir de especificações de Estrutura de Caixa (Box Structure), depois gera condições de verificação (VCs) para provar que sua implementação corresponde à especificação. Cada loop precisa de um invariante. Cada função precisa de uma pré-condição e uma pós-condição. Cada refinamento de dados precisa de uma função de abstração.

Para uma equipe tentando entregar software, isso é um imposto. Um engenheiro sênior pode gastar 40% do tempo em anotações e na estrutura de VCs, e 60% no raciocínio lógico de verdade. A estrutura não exige insight profundo. Ela exige paciência e familiaridade com a sintaxe do seu provador.

Isso é exatamente o tipo de tarefa de reconhecimento de padrões na qual os LLMs se destacam. Eles já viram milhares de invariantes de loop, métodos Dafny e arquivos SMT-LIB. Eles podem gerar anotações sintaticamente válidas que são plausíveis o suficiente para servir como ponto de partida.

O que “Automatizar Provas Formais com LLMs” Realmente Significa

Sejamos precisos. Um LLM não prova que seu código está correto. Um solucionador de provas como Z3, CVC5 ou o verificador Dafny prova que seu código está correto. O LLM automatiza o trabalho humano que fica entre seu pseudocódigo e o solucionador.

O fluxo de trabalho se parece com isso:

  1. Você escreve a implementação e a especificação.
  2. O LLM gera anotações candidatas: invariantes, pré-condições, pós-condições, variáveis ghost.
  3. Você alimenta o código anotado no verificador.
  4. O verificador ou aceita a prova, a rejeita com um contraexemplo, ou excede o tempo limite.
  5. Se a prova falhar, você inspeciona a falha e solicita ao LLM que refine a anotação.

O LLM é um estagiário muito rápido e muito confiante que conhece a sintaxe de toda ferramenta de verificação da internet. Ele vai alucinar feliz um invariante que parece perfeito e falha imediatamente. Tudo bem. O solucionador captura a alucinação. O valor está em pular o problema da página em branco.

Como os LLMs Geram Anotações que Solucionadores Podem Verificar

O truque está no prompt. Você não pede ao LLM para “provar que esta função está correta.” Você pede que ele produza um artefato específico em um formato específico.

Por exemplo, se você tem uma função semelhante a Python que calcula a soma de um array, você solicita ao LLM assim:

Given the following function and its postcondition, write a Dafny method with a loop invariant that allows the verifier to prove correctness.

Function: sum(arr) returns the sum of all elements in arr.
Postcondition: result == sum(i in 0..|arr|) arr[i]

O LLM retorna código Dafny com um invariante de loop como forall k :: 0 <= k < i ==> arr[k] is accounted for in result. Ele pode não acertar a sintaxe exata na primeira tentativa. Mas ele acerta a estrutura, e isso economiza dez minutos de digitação.

Para mais controle, você pode solicitar SMT-LIB diretamente. Isso é útil quando você está construindo pipelines de verificação personalizados em vez de usar uma linguagem de alto nível como Dafny.

Um Exemplo Funcional: Automatizando um Invariante de Loop com Python e Z3

Aqui está um exemplo completo e executável. Usamos Python para solicitar a um LLM (API da OpenAI) que gere um invariante de loop para uma função simples de soma de array, depois verificamos com Z3.

Primeiro, instale as dependências:

pip install z3-solver openai

Depois, execute o script:

import openai
from z3 import *

code = """
def sum_array(arr):
    s = 0
    i = 0
    n = len(arr)
    while i < n:
        s = s + arr[i]
        i = i + 1
    return s
"""

prompt = f"""You are a formal verification assistant.

Given this Python function that sums an array:
{code}

The postcondition is: result == Sum(arr[j] for j in range(len(arr)))

Write a Z3 SMT-LIB assertion that represents a valid loop invariant for the while loop. The invariant should mention i, s, n, and arr. Use Python Z3 syntax (ForAll, Implies, And, etc.). Return ONLY the Python code for the invariant, no explanation."""

client = openai.OpenAI()
response = client.chat.completions.create(
    model="gpt-4o",
    messages=[{"role": "user", "content": prompt}],
    temperature=0.2,
)

invariant_code = response.choices[0].message.content.strip()
print("Generated invariant:")
print(invariant_code)

# Now verify the invariant with Z3
arr = Array('arr', IntSort(), IntSort())
i, s, n = Ints('i s n')

# We manually parse the LLM's output. In production you'd use an AST parser.
# The LLM typically returns something like:
# And(0 <= i, i <= n, s == Sum([arr[j] for j in range(i)]))

# A practical check: verify that the invariant is preserved by one loop iteration
s2, i2 = Ints('s2 i2')
solver = Solver()
solver.add(n == 3)
solver.add(arr[0] == 1, arr[1] == 2, arr[2] == 3)
solver.add(i2 == 1, s2 == 1)  # assume invariant holds mid-loop

# Execute one iteration
s_next = s2 + Select(arr, i2)
i_next = i2 + 1

# Check that invariant holds after iteration
solver.add(Not(And(i_next >= 0, i_next <= n)))

if solver.check() == unsat:
    print("Invariant preserved for this concrete case.")
else:
    print("Invariant FAILED for this concrete case.")
    print(solver.model())

Este script não vai verificar a função de uma só vez. Esse é o ponto. O LLM te dá um invariante candidato. Z3 te diz se ele vale. Você itera.

Na prática, equipes que constroem pipelines de verificação assistidos por LLM encapsulam esse loop em um script que envia VCs falhos de volta ao LLM, analisa a nova anotação, executa o verificador e alimenta qualquer mensagem de erro de volta como um prompt de refinamento.

Isso não é verificação totalmente autônoma. É verificação com humano no loop e um assistente de digitação muito rápido.

Onde Isso Falha: Alucinações vs. Erros Reais

O LLM vai gerar invariantes que são fracos demais. Ele vai esquecer de mencionar uma variável que o solucionador precisa. Ele vai gerar sintaxe Dafny de 2019 que não compila mais. Ele vai dizer com confiança que i <= n é suficiente quando o loop na verdade requer i < n && s == partial_sum(arr, i).

Nenhum desses é catastrófico. O solucionador os rejeita. Você lê o erro e solicita novamente.

O perigo real é o inverso. Quando o LLM gera um invariante que é forte demais, o solucionador pode provar o programa correto contra uma especificação mais rigorosa do que a que você pretendia. Você pensa que provou que sum_array funciona para todos os arrays. Na verdade, você provou que funciona apenas para arrays onde todos os elementos são positivos, porque o LLM jogou um conjunto extra que parecia razoável.

Sempre revise a especificação gerada. O LLM escreve o boilerplate. Você é dono da lógica.

Quando Confiar na Máquina, e Quando Fazer Manualmente

Use automação com LLM para:

  • Estruturar VCs para funções diretas com pré-condições e pós-condições claras.
  • Tradução de sintaxe entre linguagens de prova. Converter uma especificação Dafny para Why3 ou SMT-LIB é mecânico e propenso a erros. Os LLMs são excelentes nisso.
  • Geração de variáveis ghost para provas de refinamento de dados. O padrão é repetitivo.

Não use automação com LLM para:

  • Provas críticas para segurança onde um bug sutil de especificação é pior do que nenhuma prova.
  • Lógica temporal complexa ou propriedades de liveness. Os dados de treinamento do LLM são mais escassos aqui, e alucinações são mais propensas a passarem despercebidas.
  • Algoritmos novos que não se parecem com nada no corpus de treinamento. Se você inventou um novo protocolo de consenso, o LLM não faz ideia de quais invariantes ele precisa.

Perguntas Frequentes

O que é uma condição de verificação na engenharia Cleanroom?

Uma condição de verificação é uma fórmula lógica gerada a partir do seu código e de sua especificação. Se a fórmula é válida, seu código implementa corretamente a especificação. Em Cleanroom, essas são tipicamente geradas antes da compilação e descarregadas usando um assistente de prova ou solucionador automatizado.

Os LLMs podem substituir assistentes de prova como Coq ou Isabelle?

Não. Os LLMs geram código e anotações que assistentes de prova podem verificar. Eles não executam os passos reais da prova. O assistente de prova ainda é a autoridade sobre se uma prova é válida.

Qual é o melhor LLM para gerar anotações de verificação formal?

GPT-4o e Claude 3.5 Sonnet têm bom desempenho na sintaxe Dafny e SMT-LIB. Modelos menores frequentemente têm dificuldades com a sintaxe precisa exigida pelos solucionadores de prova. Configure a temperatura baixa (0,1-0,2) para reduzir alucinações criativas.

Como você impede que um LLM gere uma especificação incorreta?

Você não impede. Você trata a saída do LLM como um rascunho. Sempre execute as anotações geradas pelo seu verificador. Sempre leia as pré-condições e pós-condições geradas para garantir que correspondam à sua intenção. Nunca assuma que uma verificação bem-sucedida significa que a especificação está correta.

Comece Pelas Partes Chatas

Se sua equipe está fazendo Cleanroom ou qualquer trabalho de correção por construção, a automação de maior valor não é algum grande provador de teoremas por IA. É um script que gera seus invariantes de loop e formata seu SMT-LIB para que você não precise fazer isso.

Escolha os cinco padrões de anotação mais tediosos da sua codebase. Escreva um template de prompt para cada um. Execute-os através de um LLM, verifique a saída e faça commit dos que passarem. É isso. Você acabou de recuperar 40% do seu tempo de verificação pelo custo de uma chamada de API.

As provas difíceis ainda pertencem a você. Mas pelo menos você não vai digitá-las do zero.