Compilar um smart contract não prova equivalência comportamental

Um contrato pode compilar, expor as funções esperadas e ainda executar regras diferentes do original. Em finanças programáveis, essa diferença não é um detalhe de implementação: pode alterar saldo, permissão, oferta, evento, revert ou sequência válida de transações.

Estado: Evidence Brief aprovado para publicação. Série editorial: Papers que lemos por você. Este texto analisa o preprint *SolBehave: A Behavioral Benchmark for LLM-Generated Smart Contracts*. Não afirma que a Trustyu Forge reproduziu os experimentos, que equivalência nos oráculos avaliados prova correção universal ou que os percentuais se transferem para outro modelo, prompt ou domínio.

O que o SolBehave mede

Os autores partiram de 8.360 contratos Ethereum verificados. Conseguiram reproduzir 2.098 e selecionaram 250 contratos não-proxy, com uma a vinte funções não triviais; a mediana reportada foi de 16 funções por contrato. O recorte privilegia contratos token-like e deixa de fora sistemas maiores, proxies e parte relevante da complexidade encontrada em produção.

Sete modelos open-weight receberam a tarefa de regenerar o contrato. Cada combinação teve dez gerações e uma rodada de autorreparo, com quantização de 4 bits e configuração uniforme. A comparação separou sucesso de compilação de equivalência observável.

Compilar variou de 26,4% a 92,7%

A taxa de compilação ficou entre 26,4% e 92,7%, conforme o modelo. Essa diferença já mostra que produzir um artefato sintaticamente aceito continua sensível à capacidade e à configuração. O dado mais importante, porém, aparece depois do build: no agregado, apenas 31,4% dos corpos de função que compilaram foram classificados como equivalentes no fuzzing diferencial.

Compilação responde se o artefato atende a uma gramática, tipos e regras estáticas do toolchain. Ela não responde se a transição de estado, a autorização ou os efeitos observáveis permanecem iguais.

Três oráculos procuraram divergência

O benchmark combinou três formas de observação:

1. Fuzzing diferencial: executa entradas nos contratos original e regenerado e compara saídas, estado, eventos e falhas observáveis.
2. Replay histórico: reaplica transações reais conhecidas, com 1.000 transações por contrato no experimento descrito.
3. Replay sintético orientado por dependências: cria sequências a partir de relações de leitura e escrita entre funções, buscando estados que chamadas isoladas não alcançam.

Em seis dos sete modelos, entre 13% e 31% dos contratos divergiram no replay histórico. No replay sintético orientado por dependências, a faixa ficou entre 13% e 44%. O Gemma-4-31B ficou abaixo de 3% nos dois replays reportados. Esse resultado é específico da configuração e não prova superioridade geral, ausência de falhas ou segurança do código gerado.

Equivalência observada não é segurança provada

Um contrato pode concordar em todas as entradas executadas e ainda divergir em uma sequência não gerada. Também pode reproduzir fielmente um comportamento inseguro do original. Por isso, os oráculos do SolBehave acrescentam evidência, mas não substituem especificação, análise de acesso, invariantes, auditoria de segurança e revisão de mudanças econômicas.

O replay orientado por dependências ajuda a alcançar estados compostos, mas pode perder caminhos que aceitam transações inválidas ou dependem de relações não capturadas. Comparar status, retorno e estado é uma aproximação observacional — não uma prova formal de equivalência.

Um contrato mínimo para geração e aceite

1. Fonte e direito: registre o contrato observado, versão, licença ou autorização e finalidade da reimplementação.
2. Especificação: declare invariantes de saldo, oferta, acesso, eventos, falhas e transições antes de aceitar o código.
3. Build reproduzível: fixe compilador, dependências, otimizações, rede e parâmetros.
4. Oráculos independentes: combine testes de propriedade, fuzzing diferencial, replay histórico e sequências adversariais.
5. Separação: não deixe a mesma trajetória gerar implementação e decidir sozinha se ela é equivalente.
6. Receipts: preserve modelo, prompt, artefato, bytecode, seeds, transações, divergências e decisão humana.
7. Promoção gradual: mantenha limites de valor, permissões mínimas, pausa e rollback compatíveis com o impacto.

Regra de arquitetura

O receipt “compilou” prova somente uma etapa. A promoção exige uma cadeia que ligue intenção, invariantes, build reproduzível, comportamento diferencial, segurança e aceite humano. Quando o software movimenta ativos ou executa regras irreversíveis, a ausência dessa cadeia é uma dívida de evidência, não apenas uma lacuna de teste. [R2-C3]

Na Forge, o harness deve impedir que um único sinal — compilação, teste verde ou similaridade textual — seja promovido a prova total. Evidências complementares precisam permanecer identificáveis, com fronteiras e responsáveis próprios.

Limites e conflito de interesse

O paper é um preprint submetido ao IEEE. A amostra final tem 250 contratos, deriva de um funil de 8.360 candidatos e privilegia contratos token-like com até 20 funções. As execuções começam de estado novo, o que não representa toda migração ou histórico de produção. Sete modelos open-weight, uma configuração uniforme e uma rodada de autorreparo não cobrem todos os agentes, toolchains ou estratégias possíveis.

A validação manual de dependências foi feita por um único especialista em 30 contratos e 200 relações, o que limita a estimativa de erro desse componente. Até o corte editorial, não localizamos reprodução independente completa nem contraponto público específico dos fornecedores. Os autores declaram afiliações à University of Bologna e à University of Copenhagen; não localizamos conflito comercial de fornecedor de modelo. Ausência de conflito identificado não é prova de independência absoluta.

Fontes diretas

1. SolBehave: A Behavioral Benchmark for LLM-Generated Smart Contracts — arXiv. Preprint, autores, resumo, versão e data.
2. SolBehave — texto integral. Método, funil da amostra, configurações, oráculos, resultados e limitações.

Nota editorial e de responsabilidade

Este texto combina fatos atribuídos às fontes com análise e proposta técnica do autor. Pontos de vista pessoais e profissionais não são fatos comprovados; dados, denominadores, limites, afiliações e ausência de reprodução independente são indicados quando disponíveis. O conteúdo é informativo e não substitui avaliação técnica, jurídica, financeira ou de segurança. Ethereum, contratos, produtos e modelos citados pertencem aos respectivos titulares; não há patrocínio ou endosso. Tech Human e Trustyu atuam comercialmente em desenvolvimento e governança de produtos digitais. Pesquisa, estrutura e redação tiveram assistência de IA; revisão factual, aprovação autoral e publicação foram autorizadas por Fernando Parreiras em 14/10/2026, sem revisão humana independente adicional.

Corte da pesquisa: 14/10/2026. Estado editorial: Evidence Brief especial autorizado para 27/10/2026 às 09h BRT.