Sui Prover torna-se Open Source: Por que a Verificação Formal é o elo que faltava na segurança de contratos inteligentes
Em 2025, o setor de DeFi perdeu $ 3,3 bilhões em explorações de contratos inteligentes — apesar de a maioria dos protocolos atacados ter sido auditada, alguns várias vezes. A violação de $ 1,5 bilhão da Bybit em fevereiro, a exploração de $ 42 milhões da GMX e inúmeros ataques de reentrada provaram uma verdade desconfortável: as auditorias de segurança tradicionais são necessárias, mas não suficientes. Quando a precisão matemática é fundamental, testar casos de borda não basta. É preciso prová-los.
É por isso que a abertura do código do Sui Prover importa muito mais do que apenas outro lançamento no GitHub. Desenvolvido pela Asymptotic e agora disponível gratuitamente para a comunidade de desenvolvedores Sui, o Sui Prover traz a verificação formal — a mesma técnica matemática que garante que sistemas de controle de voo e designs de processadores não falhem — para o desenvolvimento cotidiano de contratos inteligentes. Em um cenário onde um único caso de borda negligenciado pode drenar centenas de milhões, a capacidade de provar matematicamente que o código se comporta corretamente não é um luxo. Está se tornando uma necessidade.
O Paradoxo da Auditoria: Quando "Seguro" não é Seguro o Suficiente
O cenário de segurança blockchain de 2025 expôs um padrão preocupante. De acordo com o Relatório dos 100 Principais Hacks de DeFi da Halborn, protocolos que haviam passado por auditorias rigorosas ainda foram vítimas de explorações. Os motivos variaram: vulnerabilidades na cadeia de suprimentos, falhas no controle de acesso, erros matemáticos sutis em modelos econômicos. Mas o ponto comum foi que a análise de código tradicional — seja revisão manual ou varredura automatizada — não conseguiu capturar todos os modos de falha possíveis.
Considere o bug yETH da Yearn e as explorações de erro de arredondamento da Balancer. Estes não foram erros amadores. Foram erros matemáticos sutis que transformaram a precisão do arredondamento em arma através de milhares de caminhos de execução potenciais. Um auditor pode passar semanas revisando o código e ainda assim perder a única combinação de entradas que aciona um comportamento catastrófico.
A exploração da GMX ilustrou outra dimensão do problema. A vulnerabilidade não existia na lógica central de negociação — ela surgiu nas fronteiras entre os componentes, onde os oráculos se encontravam com os cálculos de margem e a lógica de liquidação interagia com a infraestrutura de ponte. Testar componentes individuais não era suficiente quando a falha surgia da interação entre eles.
É aqui que a verificação formal difere fundamentalmente das abordagens de segurança tradicionais. Em vez de verificar casos de teste específicos, a verificação formal prova matematicamente que certas propriedades se mantêm em todas as entradas e caminhos de execução possíveis. Se você puder provar que um cofre (vault) não pode ser drenado sob nenhuma circunstância, não precisa se preocupar com o caso de borda obscuro que seus testes perderam.
O que a Verificação Formal Realmente Faz
A verificação formal transforma o código em declarações matemáticas e, em seguida, prova que essas declarações correspondem a uma especificação formal do comportamento pretendido. O processo funciona assim:
Primeiro, os desenvolvedores escrevem especificações descrevendo o que seu código deve fazer — não em uma linguagem de programação, mas em uma linguagem de especificação especializada, projetada para expressar propriedades matemáticas. Para contratos inteligentes, essas especificações podem incluir declarações como "o suprimento total de tokens nunca muda, a menos que o mint ou burn seja chamado" ou "os saldos dos usuários só podem diminuir com a autorização explícita do usuário".
Em seguida, uma ferramenta de prova — neste caso, o Sui Prover, construído sobre o mecanismo de verificação Boogie e o resolvedor SMT Z3 — verifica exaustivamente se o código satisfaz essas especificações em todas as entradas possíveis. Ao contrário dos testes, que verificam valores específicos, o provador avalia todas as entradas possíveis simultaneamente por meio de raciocínio matemático.
Quando a verificação é bem-sucedida, você tem uma prova matemática de que as propriedades especificadas se mantêm. Quando falha, o provador normalmente fornece um contraexemplo — uma entrada específica que violaria a especificação, o que frequentemente revela bugs que os testes teriam perdido.
A linguagem de programação Move, usada tanto pela Sui quanto pela Aptos, foi projetada com a verificação formal em mente desde o início. Seu modelo orientado a recursos e tipagem estática forte fornecem uma base que torna a verificação formal mais prática do que em linguagens como Solidity. A Move Specification Language (MSL) permite que os desenvolvedores expressem três categorias de propriedades:
- Invariantes de Struct: Qual estado uma estrutura deve manter durante todo o seu tempo de vida
- Especificações de Função: Pré-condições, pós-condições e garantias de comportamento para cada função
- Especificações de Estado Global: Propriedades em todo o sistema que devem ser mantidas em todas as transições de estado
Sui Prover: De Ferramenta Interna a Recurso da Comunidade
A Asymptotic desenvolveu inicialmente o Sui Prover para apoiar seu trabalho de auditoria em protocolos construídos na Sui. Como o único provedor de verificação formal na Sui, eles precisavam de ferramentas que pudessem ir além da revisão manual para verificar matematicamente áreas de alto risco das bases de código dos clientes.
A decisão de abrir o código da ferramenta reflete tanto a maturidade da tecnologia de verificação formal quanto o reconhecimento de que a segurança é um bem público. Quando mais desenvolvedores podem acessar a verificação formal, todo o ecossistema se torna mais seguro — o que beneficia a todos, incluindo auditores de segurança que podem se concentrar em preocupações de nível superior.
O Sui Prover está disponível no GitHub e pode ser instalado via Homebrew (brew install asymptotic-code/sui-prover/sui-prover). O desenvolvimento ativo continua, com problemas recentes abertos em janeiro de 2026 abordando melhorias contínuas.
O que torna o Sui Prover particularmente valioso é sua integração com o fluxo de trabalho de desenvolvimento existente do Sui Move. Os desenvolvedores podem adicionar especificações ao seu código existente de forma incremental, verificando funções críticas primeiro enquanto expandem gradualmente a cobertura. As especificações cumprem uma função dupla como verificações de segurança e documentação — qualquer pessoa que revise ou integre o contrato pode ler as especificações para entender os comportamentos garantidos.
Propriedades do Mundo Real que Você Pode Provar
O poder da verificação formal torna-se concreto quando você considera propriedades específicas que podem ser provadas:
Vaults Não Drenáveis: Para protocolos DeFi que custodiam fundos de usuários, provar que nenhuma sequência de operações pode esvaziar o vault sem a devida autorização elimina categorias inteiras de ataques. Isso não é "testamos muitos vetores de ataque" — é a certeza matemática de que a drenagem é impossível.
Preços de Cotas Não Decrescentes: Yield vaults e pools de liquidez frequentemente precisam garantir que os preços das cotas nunca diminuam inesperadamente (fora do slippage esperado). A verificação formal pode provar que esta propriedade se mantém, independentemente das condições de mercado ou das ações dos usuários.
Preservação Exata de Saldo: Contratos de tokens podem provar que o suprimento total permanece constante em todas as operações, que as transferências movem exatamente a quantia especificada e que nenhum token é criado ou destruído, exceto por meio de funções designadas.
Garantias de Controle de Acesso: Provar que apenas endereços autorizados podem chamar funções privilegiadas, independentemente do estado do contrato ou da sequência de operações anteriores.
Invariantes Econômicos: Protocolos DeFi complexos podem provar propriedades sobre seus modelos econômicos — que as restrições de liquidez são respeitadas, que os índices de colateralização são mantidos e que loops de arbitragem não podem extrair valor ilimitado.
Esses não são exemplos teóricos. Desenvolvedores no ecossistema Sui já aplicaram especificações formais para verificar contratos DeFi, incluindo AMMs e sistemas de yield farming alavancado. Quando essas propriedades são provadas em vez de presumidas, a postura de segurança muda fundamentalmente.
O Cenário de Segurança Exige Melhores Ferramentas
As estatísticas de 2025 tornam o caso da verificação formal convincente. De acordo com pesquisadores de segurança, incidentes off-chain representaram 56,5 % dos ataques e 80,5 % dos fundos perdidos em 2024, mas as vulnerabilidades de contratos inteligentes continuam sendo devastadoras quando exploradas. Vulnerabilidades de controle de acesso sozinhas causaram $ 953,2 milhões em danos documentados ao longo de 2024.
O OWASP Smart Contract Top 10 para 2025 documentou mais de $ 1,42 bilhão em perdas coletivas em ecossistemas descentralizados. Ferramentas de segurança tradicionais — Mythril para execução simbólica, Echidna para fuzzing baseado em propriedades, auditorias manuais de firmas como OtterSec, Halborn e MoveBit — abordam diferentes aspectos do problema. Mas, à medida que os protocolos se tornam mais complexos e gerenciam mais valor, as lacunas entre essas abordagens tornam-se mais perigosas.
A CertiK implantou técnicas de verificação formal para verificar matematicamente contratos inteligentes, protegendo mais de $ 300 bilhões em ativos, de acordo com seus relatórios. Essa escala demonstra tanto a demanda por garantias de segurança matemática quanto a viabilidade de aplicar métodos formais a sistemas de blockchain.
O consenso emergente entre pesquisadores de segurança é que auditorias, bug bounties, monitoramento, lançamentos graduais e métodos formais devem trabalhar juntos como camadas de defesa. Para sistemas de alto valor, a verificação formal de invariantes críticos está se tornando uma prática padrão, em vez de um rigor excepcional.
Por que o Move Torna a Verificação Formal Prática
Nem todas as linguagens de programação são igualmente adequadas para a verificação formal. A flexibilidade do Solidity e a complexidade da EVM tornam a verificação formal desafiadora — possível, mas exigindo sobrecarga significativa de ferramentas e especialização.
O Move foi projetado de forma diferente. Seu modelo orientado a recursos significa que os ativos possuem tipos lineares que não podem ser duplicados ou descartados implicitamente. O sistema de tipos captura categorias inteiras de bugs em tempo de compilação que exigiriam verificações em tempo de execução em outras linguagens. O Move Prover foi desenvolvido juntamente com a linguagem, garantindo uma integração estreita entre os recursos da linguagem e as capacidades de verificação.
Essa herança de design significa que as próprias bibliotecas padrão do Move foram formalmente verificadas. Quando você constrói na Sui ou na Aptos, está construindo sobre uma base que possui provas matemáticas de correção — provas que se acumulam à medida que você adiciona seu próprio código verificado por cima.
A implicação prática: a verificação formal no Move exige menos conhecimento especializado do que em outras plataformas. A documentação do Sui Prover, os exemplos e a integração com fluxos de trabalho de desenvolvimento padrão tornam-no acessível a desenvolvedores que não são especialistas em métodos formais. Você pode aprender a escrever especificações de forma incremental, começando com contratos de função simples e progredindo para invariantes complexos conforme seu entendimento se aprofunda.
O Que Isso Significa para Desenvolvedores Sui
Para desenvolvedores que constroem na Sui, o Sui Prover de código aberto cria novas possibilidades:
Diferenciação de Segurança: Em um cenário DeFi competitivo, provar propriedades de segurança não é apenas mitigação de risco — é uma vantagem competitiva. Usuários e auditores podem verificar alegações sobre a segurança do protocolo em vez de confiar em afirmações.
Custos de Auditoria Reduzidos: Quando funções críticas possuem provas formais, os auditores podem se concentrar em preocupações de nível superior em vez de testar exaustivamente casos extremos. Isso pode reduzir o escopo e o custo da auditoria, melhorando efetivamente os resultados de segurança.
Qualidade da Documentação: Especificações formais são documentações precisas que não ficam obsoletas. Quando a especificação diz que uma função preserva um determinado invariante, isso é provável ou o prover sinalizará uma violação.
Adoção Incremental: Você não precisa verificar formalmente tudo. Comece com as funções de maior risco — aquelas que lidam com retiradas, colaterais ou operações privilegiadas — e expanda a cobertura ao longo do tempo.
O ecossistema Sui já abriga várias firmas de auditoria experientes, incluindo MoveBit (pioneira em verificação formal de Move), Certora, OtterSec e Zellic. O Sui Prover adiciona uma ferramenta que os desenvolvedores podem usar diretamente, sem necessariamente contratar auditores externos para cada tarefa de verificação.
A Trajetória Mais Ampla
O código aberto do Sui Prover se encaixa em um padrão mais amplo de amadurecimento das ferramentas de segurança em toda a indústria de blockchain. A verificação formal está deixando a pesquisa acadêmica para se tornar infraestrutura de produção, passando de consultorias especializadas para ferramentas acessíveis aos desenvolvedores.
Essa trajetória é importante porque a escala do valor protegido por contratos inteligentes continua a crescer. Protocolos DeFi gerenciam coletivamente centenas de bilhões em ativos. Um único bug em um protocolo importante pode causar perdas que excedem o que empresas de software tradicionais enfrentam em toda a sua existência.
A indústria de software tradicional acabou adotando métodos formais para sistemas de segurança crítica — aviônica, dispositivos médicos, sistemas financeiros. A indústria de blockchain, onde "o código é a lei" e os bugs são frequentemente irreversíveis, tem motivos ainda mais fortes para adotar a verificação matemática.
O Sui Prover representa um passo nessa direção: tornar a verificação formal acessível o suficiente para que os desenvolvedores realmente a utilizem, em vez de relegá-la a uma documentação de "teatro de segurança" que ninguém lê.
Primeiros Passos
Para desenvolvedores interessados em explorar a verificação formal na Sui:
- Instale o Sui Prover:
brew install asymptotic-code/sui-prover/sui-prover - Comece Pequeno: Adicione especificações a uma única função crítica e verifique se ela é aprovada
- Aprenda a Linguagem de Especificação: A Move Specification Language possui uma excelente documentação para expressar propriedades comuns
- Itere: Expanda a cobertura para mais funções e invariantes mais complexos à medida que ganha confiança
O investimento no aprendizado da especificação formal rende dividendos compostos. Uma vez que você tenha verificado que os módulos de nível inferior estão corretos, você pode construir lógica de nível superior sabendo que essas bases estão matematicamente comprovadas.
Para uma indústria que perdeu bilhões para bugs evitáveis em 2025, a questão não é se a verificação formal vale o esforço. A questão é quão rapidamente o ecossistema pode adotá-la. O lançamento em código aberto do Sui Prover remove uma barreira — agora o conhecimento e a prática precisam seguir o exemplo.
Construir aplicações seguras na Sui exige uma infraestrutura confiável que corresponda aos padrões de segurança do seu protocolo. BlockEden.xyz fornece endpoints RPC de nível empresarial para Sui, Aptos e mais de 20 redes com o tempo de atividade e a confiabilidade que as aplicações em produção exigem. Explore nosso marketplace de APIs para impulsionar seus contratos inteligentes verificados formalmente.