VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus

O artigo apresenta o VeriStruct, um novo quadro de trabalho que estende a verificação automatizada assistida por IA para módulos de estruturas de dados complexos em Verus, utilizando um planejador para gerar especificações e um mecanismo de reparo para corrigir erros de sintaxe, alcançando uma taxa de sucesso de 99,2% na verificação de funções em módulos Rust.

O essencial

Imagine que você é um arquiteto construindo um arranha-céu (o software) usando blocos de Lego muito complexos (o código). Você quer ter certeza absoluta de que o prédio não vai desabar, que as portas não vão trancar sozinhas e que ninguém vai cair da janela.

No mundo da computação, isso se chama verificação formal. É como ter um inspetor de obras super rigoroso que usa matemática pura para provar que seu prédio é seguro. O problema é que, para usar esse inspetor, você precisa escrever um manual de instruções extremamente detalhado e difícil (chamado de "anotações" ou "especificações") explicando exatamente como cada bloco deve funcionar. Fazer isso manualmente é tão trabalhoso que poucas pessoas o fazem.

Aqui entra o VeriStruct, a "estrela" deste artigo.

O Que é o VeriStruct?

Pense no VeriStruct como um assistente de construção com inteligência artificial que não apenas lê o manual, mas escreve o manual para você.

O objetivo dele é pegar um código de computador (feito na linguagem Rust) e adicionar todas aquelas anotações matemáticas necessárias para provar que o código é perfeito, sem erros e sem falhas de segurança.

O Grande Desafio: De "Uma Sala" para "Um Edifício Inteiro"

Antes do VeriStruct, a IA conseguia ajudar a verificar apenas uma sala de cada vez (uma função simples de código). Mas os programas reais são feitos de estruturas de dados complexas, como listas, filas e mapas, que são como edifícios inteiros com muitas salas conectadas.

Verificar um "edifício" inteiro é muito mais difícil porque:

1. Precisa de um mapa abstrato: Você não pode descrever cada tijolo. Você precisa de uma visão geral (ex: "isto é uma fila de espera").
2. Precisa de regras de segurança: Você precisa garantir que, não importa o que aconteça, o elevador nunca vai abrir no andar errado (chamado de "invariantes de tipo").
3. A IA se confunde: As IAs atuais (como o ChatGPT) são ótimas em escrever código, mas quando tentam escrever as regras matemáticas para o Verus (o inspetor de obras), elas frequentemente usam a gramática errada ou esquecem regras importantes.

Como o VeriStruct Funciona (A Analogia do Chefe de Obra)

O VeriStruct não é apenas uma IA que chuta o código. Ele funciona como um Chefe de Obra muito organizado que divide o trabalho em duas etapas principais:

1. O Planejamento (O "Planner")

Antes de começar a escrever, o VeriStruct tem um "cérebro" que analisa o código e diz: "Ok, para este módulo, precisamos de um mapa (View), precisamos de regras de segurança (Invariantes) e precisamos de especificações para cada porta (Funções). Vamos focar nisso!".
Isso evita que a IA tente fazer tudo de uma vez e se perca.

2. A Construção e o "Conserto" (Geração e Reparo)

Aqui está a mágica do VeriStruct:

• Geração: Ele pede para a IA escrever as regras.
• O Erro: A IA quase sempre erra algo na primeira tentativa (como usar uma palavra proibida ou esquecer uma regra).
• O Reparo Automático: Em vez de desistir, o VeriStruct pega o erro, olha para ele e diz: "Ah, você tentou usar uma função proibida aqui. Vamos consertar isso criando uma versão especial dessa função que o inspetor aceita."

Ele faz isso em um ciclo: Escreve -> Tenta verificar -> Se errar, conserta -> Tenta de novo. É como um encanador que, ao ver que a torneira vazou, não joga a torneia fora, mas ajusta a rosca e tenta de novo até que pare de vazar.

O Resultado: Um Edifício à Prova de Falhas

Os autores testaram esse sistema em 11 estruturas de dados diferentes (como filas de espera, árvores de dados e travas de segurança).

• O resultado: O VeriStruct conseguiu verificar 99,2% de todas as funções desses módulos.
• Comparação: Se você apenas pedisse para uma IA comum tentar fazer isso sem o sistema de planejamento e reparo, ela teria sucesso em apenas cerca de 40% dos casos.

Por que isso é importante?

Hoje em dia, muita gente está usando IAs para escrever código. Isso aumenta a produtividade, mas também aumenta o risco de criar softwares cheios de buracos de segurança.

O VeriStruct é como um filtro de segurança automático. Ele garante que, mesmo que a IA tenha escrito o código ou ajudado a escrever, o resultado final é matematicamente provado como seguro. Isso é crucial para coisas críticas, como sistemas bancários, controle de tráfego aéreo ou carros autônomos, onde um erro pode custar muito caro.

Resumo da Ópera:
O VeriStruct é um sistema inteligente que ensina a IA a escrever os "manuais de segurança" matemáticos para softwares complexos, consertando seus próprios erros no processo, garantindo que o código final seja tão seguro quanto um arranha-céu construído com a mais alta precisão de engenharia.

Resumo técnico

1. O Problema

A verificação formal de programas é uma técnica poderosa para garantir a correção e segurança de software, mas sua adoção prática é limitada pela enorme dificuldade em criar anotações lógicas manuais (pré-condições, pós-condições, invariantes e blocos de prova). Embora a Inteligência Artificial Generativa (LLMs) tenha demonstrado sucesso em verificar algoritmos simples de "livro didático" (funções únicas), ela enfrenta desafios significativos ao lidar com módulos de estruturas de dados complexos.

Os principais obstáculos identificados são:

• Complexidade Estrutural: Estruturas de dados exigem não apenas especificações de funções, mas também abstrações matemáticas (Views) para representar o estado lógico e invariantes de tipo que devem ser preservados por todas as operações.
• Limitações de Sintaxe e Semântica: Os LLMs frequentemente falham ao entender a sintaxe especializada e a semântica de verificação da linguagem Verus (uma extensão de verificação para Rust), como a distinção entre funções executáveis e funções de especificação (spec).
• Falta de Contexto: Abordagens anteriores focavam em gerar um único artefato de especificação, enquanto estruturas de dados exigem a geração coordenada de múltiplos componentes interdependentes.

2. Metodologia: O Framework VeriStruct

O VeriStruct é um framework de verificação automatizada assistida por IA que estende o trabalho anterior (AutoVerus) para lidar com módulos completos de estruturas de dados em Verus. O sistema opera em um pipeline de duas etapas, orquestrado por um módulo planejador:

A. Entrada e Saída

• Entrada: Código fonte Rust da estrutura de dados (sem anotações) e uma suíte de testes unitários que define o comportamento esperado.
• Saída: Uma versão do código totalmente anotada e verificada pelo Verus.

B. Etapa 1: Geração de Anotações (Stage 1)

O sistema utiliza um Módulo Planejador para analisar o código e decidir quais componentes de anotação são necessários. Em seguida, invoca módulos especializados sequencialmente:

1. Módulo View (Visão): Gera uma trait View que mapeia a implementação concreta para uma abstração matemática (ex: sequências, conjuntos), permitindo raciocínio lógico sobre a estrutura.
2. Módulo Invariante de Tipo: Gera invariantes que devem ser verdadeiros para todas as instâncias da estrutura (ex: limites de índices, capacidade).
3. Módulo de Especificações: Gera pré-condições (requires) e pós-condições (ensures) para os métodos.
4. Módulo de Blocos de Prova: Gera blocos de prova (proof blocks) e invariantes de loop para auxiliar o verificador.

• Refinamento de View: O sistema inclui um passo de refinamento para evitar que o LLM crie "Views" triviais (que apenas expõem todos os campos). O prompt instrui o modelo a criar abstrações concisas e logicamente coerentes.
• Guia de Sintaxe: Os prompts incluem diretrizes estruturadas extraídas da documentação oficial do Verus para mitigar erros de sintaxe.

C. Etapa 2: Reparo Iterativo (Stage 2)

Como a geração inicial raramente é perfeita, o VeriStruct executa um loop de reparo:

1. O código anotado é submetido ao verificador Verus.
2. Se houver erros, o sistema classifica a mensagem de erro e seleciona um Módulo de Reparo específico (ex: reparo de uso incorreto de funções executáveis em especificações, inconsistências de mutabilidade, falhas em testes).
3. O módulo de reparo gera uma nova tentativa de anotação.
4. O processo repete até que a verificação seja bem-sucedida ou o orçamento de iterações seja esgotado.

3. Contribuições Chave

1. Novo Fluxo de Trabalho para Estruturas de Dados: Introdução de um pipeline LLM-assistido capaz de sintetizar não apenas especificações de funções, mas também abstrações matemáticas (Views) e invariantes de tipo para módulos complexos.
2. Implementação VeriStruct: A criação de uma ferramenta que integra planejamento, geração modular e reparo automatizado de erros de verificação.
3. Abordagem Híbrida de Reparo: Desenvolvimento de módulos de reparo especializados que vão além da correção de blocos de prova, abordando erros de Views, invariantes e especificações, além de usar um planejador para evitar a geração de componentes desnecessários.

4. Resultados

O framework foi avaliado em 11 benchmarks de estruturas de dados em Rust (incluindo RingBuffer, Treemap, Bitmap, RwLock, etc.), totalizando 129 funções a serem verificadas.

• Taxa de Sucesso: O VeriStruct verificou com sucesso 10 dos 11 benchmarks (90,9%).
• Cobertura de Funções: Verificou 128 das 129 funções (99,2%).
• Comparação com Baselines:
  • O VeriStruct superou significativamente uma baseline simples (que apenas itera chamadas de LLM sem planejamento estruturado), que conseguiu verificar apenas 52 funções (40%).
  • Superou também o agente autônomo Claude Code (usando Claude Sonnet 4.5), que verificou 102 funções.
• Eficiência: O VeriStruct alcançou melhores resultados com um custo de tokens comparável ou inferior ao do Claude Code, demonstrando que a estruturação do fluxo de trabalho é mais eficiente do que apenas aumentar a capacidade do modelo.
• Estudo de Caso (Bitmap): O sistema foi capaz de encontrar uma abstração diferente (e mais simples) da solução humana para o benchmark de Bitmap, demonstrando flexibilidade criativa.

5. Significado e Impacto

O trabalho representa um avanço crucial rumo à verificação formal automatizada em escala. Ao demonstrar que é possível verificar módulos de bibliotecas de estruturas de dados (que são a base de muitos sistemas de software), o VeriStruct reduz a barreira de entrada para a adoção de métodos formais.

• Confiança em Código Gerado por IA: Oferece um mecanismo para validar a correção de código escrito ou assistido por IA, mitigando riscos de segurança.
• Reutilização de Código Verificado: Ao verificar bibliotecas de estruturas de dados, permite que o código cliente confie nessas componentes, simplificando a verificação de sistemas maiores.
• Futuro: O artigo sugere direções futuras como o uso de Retrieval-Augmented Generation (RAG) para encontrar lemas na biblioteca padrão do Verus, síntese de álgebra de recursos para concorrência e o uso de Aprendizado por Reforço (RL) para otimizar a busca por especificações.

Em resumo, o VeriStruct preenche a lacuna entre a verificação manual rigorosa e a geração automática de código, provando que, com a orquestração correta de LLMs e ferramentas de verificação, é possível automatizar a correção de software complexo.