Resumo Técnico: Combinando Inferência de Especificação Mecânica e Agente para Move

Declaração do Problema

A verificação formal de contratos inteligentes Move usando o Move Prover (MVP) enfrenta um gargalo prático significativo: o alto custo de escrever especificações manualmente. Embora os desenvolvedores visem verificar propriedades de alto nível (por exemplo, invariantes de estado global, conservação de fundos ou abortos condicionais), o processo de verificação exige pré e pós-condições explícitas e de baixo nível para cada função de suporte. Escrever essas especificações é mecânico, tedioso e frequentemente domina o custo de usar um verificador, impedindo uma adoção mais ampla. Embora o MVP possa incorporar corpos de função para verificar chamadas não especificadas, essa abordagem não escala para verificação modular.

Metodologia

O artigo apresenta uma ferramenta inovadora que combina análise mecânica da pré-condição mais fraca (WP) com codificação agente (especificamente via Claude Code) para inferir especificações para bytecode Move. O sistema opera por meio de um fluxo de trabalho colaborativo onde o Move Prover atua como um oráculo para sinais tanto mecânicos quanto gerados por IA.

1. Componente Mecânico: Análise de Pré-condição Mais Fraca (WP)

A base mecânica depende de uma análise WP padrão realizada sobre o bytecode Move. As principais características técnicas incluem:

• Eliminação de Referências: Antes da análise, o pipeline de transformação do Move Prover elimina referências no estilo Rust (&T, &mut T) reescrevendo o bytecode em uma forma intermediária livre de referências. Referências compartilhadas são incorporadas e referências mutáveis são convertidas em parâmetros de entrada/saída. Isso permite que o raciocínio clássico no estilo de Dijkstra seja aplicado diretamente.
• Instrumentação de Especificação: O bytecode é instrumentado com declarações assume e assert derivadas de especificações de usuário existentes. As chamadas são instrumentadas usando predicados comportamentais (por exemplo, result_of, aborts_of) para abstrair contratos de chamadas.
• Saída: O motor WP deriva mecanicamente condições de abort, cláusulas modifies e pós-condições no estilo de consequência. No entanto, ele luta com invariantes de loop, que geralmente não são deriváveis apenas dos corpos de loop; sem essas, as especificações inferidas tornam-se vazias.

2. Componente Agente: Inferência Guiada por IA

Um agente de codificação com IA (Claude Code), integrado via um serviço de Protocolo de Contexto de Modelo (MCP), aborda as limitações do motor WP:

• Invariantes de Loop: O agente usa reconhecimento de padrões para propor invariantes indutivos (por exemplo, monotonicidade, conservação de somas, prefixos ordenados) que o motor WP não consegue derivar.
• Idioms de Alto Nível: O agente gera especificações de alto nível (por exemplo, monotonicidade, invariantes estruturais) em idiomais familiares aos desenvolvedores humanos.
• Simplificação: O agente refina as especificações verbosas, semanticamente corretas, mas frequentemente intratáveis, geradas pelo motor WP em formas mais compactas e legíveis.
• Dicas de Prova: Quando a verificação expira (por exemplo, devido a aritmética não linear), o agente gera lemas e dicas de prova para guiar o provador.

3. O Fluxo de Trabalho

O processo é entregue como um plugin do Claude Code utilizando "habilidades" (instruções em Markdown), ganchos no momento da edição e um servidor MCP. O fluxo de trabalho segue uma sequência fixa de tarefas:

1. Sintetizar Invariantes de Loop: O agente identifica loops sem invariantes e os propõe.
2. Inferir Pré-condições Mais Fracas: O agente chama o MVP via MCP para gerar especificações de base mecânica.
3. Simplificar: O agente reescreve as especificações combinadas para legibilidade e concisão.
4. Verificação e Refinamento: Uma execução de verificação de escopo total é realizada. Se erros lógicos forem encontrados, o agente os corrige. Se ocorrerem expirações, o agente introduz lemas ou dicas de prova.
5. Iteração: Contra-exemplos do provador alimentam o agente de volta para refinamento. O usuário pode intervir a qualquer momento.

Contribuições Principais

O artigo identifica três contribuições principais:

1. Arquitetura de Inferência Híbrida: Até onde os autores sabem, este é o primeiro sistema de inferência de especificação baseado em LLM a combinar uma base mecânica sólida (WP) com um componente agente. O motor WP lida com a derivação mecânica (abortos, modificações, pós-condições), enquanto a IA lida com as partes "mais fracas" do WP (invariantes de loop e idiomais de alto nível).
2. Integração de Agente de Codificação Interativo: Ao contrário de ferramentas de inferência anteriores que operam como scripts autônomos, este sistema é integrado como um plugin em um agente de codificação interativo (Claude Code). Isso permite um loop colaborativo onde o usuário pode monitorar, substituir ou contribuir para o processo de inferência.
3. Eliminação de Referências para WP: O artigo detalha a aplicação da eliminação de referências (anteriormente usada no Aeneas para Rust) ao bytecode Move para habilitar a análise WP clássica. Essa combinação de formas intermediárias livres de referências com inferência WP não foi descrita anteriormente.

Resultados e Avaliação

A ferramenta foi aplicada a um corpus de código Move canônico, incluindo:

• Funções de ordem superior: Especificamente, uma função de busca em vetores usando predicados.
• Aritmética: Uma função de exponenciação envolvendo aritmética não linear e verificações de overflow.
• Algoritmos dependentes de estado: Uma função que modifica armazenamento global em vários endereços.

Observações:

• A abordagem híbrida gerou com sucesso especificações para cenários complexos envolvendo loops, despacho dinâmico e estado global.
• No exemplo de exponenciação, o motor WP forneceu a condição de correção, enquanto o agente introduziu com sucesso um lema de monotonicidade para resolver uma expiração de verificação.
• O agente frequentemente reescreveu especificações geradas pelo WP em formas mais compactas, mesmo após a própria simplificação de termos do motor WP.
• O sistema lida com condições "vazias" fazendo com que o agente as descarte durante a fase de simplificação.

Significado e Alegações

O artigo enquadra este trabalho como trabalho inicial e um artigo de ferramentas com resultados preliminares. Os autores fazem alegações modestas quanto ao significado:

• Forças Complementares: O sistema aproveita a confiabilidade da dedução mecânica para boilerplate e as capacidades de reconhecimento de padrões de LLMs para raciocínio indutivo. A base WP impede que o agente sugira especificações "completamente erradas", enquanto o agente preenche as lacunas onde o WP falha.
• Inovação no Fluxo de Trabalho: A integração da verificação em um loop de codificação conversacional por meio de habilidades e MCP representa uma mudança de ferramentas de análise estática para fluxos de trabalho dinâmicos e colaborativos.
• Direção Futura: Os autores reconhecem que a definição de "habilidades" (instruções) é uma área em evolução. Eles planejam aplicar a ferramenta retrospectivamente ao Framework Aptos e a um motor complexo de negociação perpétua para avaliar a escalabilidade e os custos de tokens em comparação com especificações escritas à mão. Eles observam explicitamente que a eficácia da abordagem híbrida em comparação com a inferência pura de LLM requer mais estudo sistemático.

O artigo conclui que esta metodologia demonstra um caminho viável para reduzir o custo de boilerplate da verificação formal em Move, permitindo uma colaboração entre IA, dedução mecânica e desenvolvedores humanos.