Inferência de invariantes de loops em especificações formais de smart contracts solidity utilizando LLMs em framework de geração e verificação

Abstract

A verificação formal de contratos inteligentes é fundamental para garantir a segurança de ativos financeiros em redes Blockchain, onde falhas de software podem resultar em perdas irreversíveis. Um dos maiores desafios nesse processo é a validação de programas contendo loops, cuja verificação automática depende da identificação de invariantes de loop, uma tarefa historicamente complexa e, em geral, indecidível. Nesse contexto, tais invariantes atuam como premissas em Triplas de Hoare, permitindo decompor a prova de correção do laço em condições lógicas de alcançabilidade, indutividade e provabilidade da pós-condição. Embora abordagens neuro-simbólicas recentes, como o framework LLM and Model checking for loop Invariant inference (LaM4Inv), tenham demonstrado sucesso na inferência automática desses invariantes para a linguagem C, não existiam até então soluções para Solidity, a linguagem mais utilizada para implementar contratos inteligentes em Blockchain. O LaM4Inv utiliza o framework Code2Inv para gerar as condições necessárias de verificação dos invariantes candidatos. Este trabalho apresenta uma adaptação do LaM4Inv. Desenvolvemos um Gerador de Condições de Verificaçãos (VCs), baseado na abordagem do Code2Inv, capaz de traduzir a representação intermediária (usada pela ferramenta Slither, que é um analisador estático para smart contracts em Solidity) para fórmulas Satisfiability Modulo Theories (SMT), permitindo a validação rigorosa de candidatos a invariantes gerados por Large Language Modelss (LLMs). Implementamos uma estratégia de orquestração sequencial de modelos para otimizar custos e eficiência. A avaliação experimental em 312 contratos demonstrou uma taxa de sucesso de 100% na inferência automática, validando a eficácia da abordagem proposta para viabilizar a verificação formal autônoma de loops em contratos inteligentes. O código está publicamente disponível em https://github.com/almirmcunhajr/solidity-lam4inv.