A Rust-to-Lean Verification Pipeline with AI Provers: An Experience Report

Resumo Técnico: Um Pipeline de Verificação de Rust para Lean com Provedores de IA

Declaração do Problema
O código criptográfico de produção, particularmente dentro de stacks de máquinas virtuais de conhecimento zero (zkVM) como as utilizadas no Ethereum, tolera quase nenhum erro. Métodos tradicionais de verificação — revisão de código, fuzzing e testes baseados em propriedades — possuem limitações estruturais: dependem da antecipação de padrões específicos de bugs ou da exploração de orçamentos finitos de entrada, frequentemente perdendo divergências semânticas silenciosas. Embora a verificação formal ofereça provas verificadas por máquina para todas as entradas, seu custo histórico tem sido proibitivo, exigindo anos de esforço para acoplar implementação e prova em sistemas como seL4 ou CompCert. Além disso, as ferramentas existentes de verificação de Rust (por exemplo, Verus, Prusti, Kani) frequentemente visam fragmentos específicos da linguagem ou dependem de solvers SMT sem conectar o Rust de produção às especificações matemáticas abstratas necessárias para protocolos criptográficos.

Metodologia
Os autores propõem e implementam um pipeline de verificação neurosimbólica que integra três componentes distintos para conectar código Rust de produção e provas verificadas por máquina em Lean 4:

1. Extração Simbólica: O pipeline eleva código Rust seguro para Lean 4 puramente funcional usando ferramentas de extração.
   • Aeneas/Charon: Traduz Rust seguro através de uma representação intermediária tipada (LLBC) para Lean 4, tratando garantias do verificador de empréstimo como entradas semânticas e envolvendo operações em um monad Result.
   • Hax: Uma ferramenta baseada em anotações que traduz Rust (via THIR) para Lean 4, F⋆ ou Rocq.
2. Especificações Formais: O código extraído é verificado contra alvos matemáticos abstratos fornecidos por bibliotecas especializadas:
   • ArkLib: Formaliza argumentos concisos não interativos de conhecimento (SNARKs) e Reduções de Oráculo Interativo (IORs), incluindo protocolos como FRI, Sum-Check e WHIR.
   • CompPoly: Fornece teoria de polinômios computacionais e de corpos finitos.
3. Provedores de IA: O pipeline emprega agentes de IA (Aristotle e Aleph) para fechar obrigações de prova geradas durante a verificação. Esses agentes decompõem objetivos, geram lemas candidatos e constroem provas. Crucialmente, o kernel Lean re-verifica cada prova, garantindo que a saída da IA não comprometa a correção.

O fluxo de trabalho prossegue em quatro etapas: (1) Extração de Rust para Lean 4; (2) Definição de especificação (seja escrita à mão ou via equivalência de biblioteca); (3) Construção de prova (manual, assistida por IA ou híbrida); e (4) Re-verificação pelo kernel.

Principais Contribuições
O artigo faz quatro contribuições primárias:

• Integração de Pipeline: Documenta a primeira integração bem-sucedida de ferramentas de extração de Rust para Lean, bibliotecas criptográficas formais e provedores de IA em um único fluxo de trabalho ponta a ponta.
• Aplicação a Primitivas Criptográficas: O pipeline foi aplicado a oito alvos críticos para consenso dentro do Projeto de Verificação zkEVM da Fundação Ethereum, especificamente em Plonky3 (dobramento FRI, aritmética de campos Mersenne31/KoalaBear, avaliação Horner, agendamento de rodadas) e RISC Zero (verificação de inclusão em Merkle).
• Análise Empírica de Provedores de IA: Os autores fornecem um relato ao nível de lema do desempenho da IA. Eles relatam que provedores de IA (especificamente Aleph) fecharam com sucesso dois teoremas não triviais do estilo de limites na função compute_log_arity_for_round do Plonky3. Essas provas envolveram a decomposição de ligações monádicas e o tratamento de limites condicionais, produzindo lemas auxiliares reutilizáveis.
• Documentação da Lacuna de Engenharia: O artigo identifica pontos de atrito específicos, incluindo a deriva da cadeia de ferramentas Lean 4 entre diferentes ferramentas, limites de extração no Aeneas/Hax (por exemplo, problemas com traits genéricas, crates externas e loops while), e lemas ausentes em bibliotecas padrão. Propõe três soluções alternativas: correções a montante, extração de modelos semânticos e ferramentas em camadas para código inseguro.

Resultados

• Verificação Bem-Sucedida: O pipeline verificou com sucesso que as implementações em Rust de primitivas criptográficas são equivalentes às suas especificações matemáticas no ArkLib e CompPoly.
• Desempenho da IA: No exemplo em execução (compute_log_arity_for_round), o Aleph fechou automaticamente dois teoremas anteriormente não resolvidos (arity_respects_max_bound e arity_respects_target_distance) gerando provas estruturadas com lemas auxiliares.
• Limitações Observadas: Os provedores de IA performaram bem em lemas estruturais de fluxo de controle, aritmética linear com condições laterais suaves e simplificação de boilerplate. No entanto, lutaram com identidades algébricas específicas do domínio que exigiam seleção específica de lemas do Mathlib4, invariantes de loop em funções recursivas e obrigações que exigiam axiomatização de interface externa. Essas áreas permaneceram como tarefas manuais.
• Disponibilidade do Artefato: Todo o código, especificações e provas são públicos, incluindo repositórios para verificações baseadas em Aeneas e baseadas em Hax.

Significado e Alegações
O artigo alega documentar a primeira tentativa de combinar esses três fios tecnológicos (extração, bibliotecas formais, provedores de IA) para Rust criptográfico do mundo real. Seu significado reside em demonstrar um pipeline funcional onde:

1. A correção é preservada: A saída da IA é estritamente validada pelo kernel Lean.
2. A produtividade é aprimorada: A IA atua como um multiplicador para obrigações estruturais e aritméticas, embora engenheiros humanos permaneçam essenciais para o design de especificação, descoberta de invariantes e seleção de abstrações matemáticas.
3. Barreiras são reduzidas: A abordagem oferece um caminho para uma verificação formal mais eficaz de sistemas de produção, indo além do modelo de "muitos anos-homem" de verificação rigidamente acoplada visto em sistemas anteriores de referência.

Os autores permanecem modestos, observando que, embora a IA tenha fechado lemas não triviais específicos, a forma fundamental do esforço de verificação (especificação e abstração) permanece uma tarefa de engenharia humana. Eles posicionam este trabalho como um passo para reduzir barreiras de adoção e facilitar uma integração mais eficaz de IA em pipelines de verificação formal.