Uma Prova de Conceito para a Verificação Formal de Contratos Inteligentes
Murilo de Souza Neves, Adilson Luiz Bonifacio
TL;DR
Este trabalho aborda o desafio de garantir a confiabilidade de contratos inteligentes diante de sua imutabilidade. Propõe uma abordagem de verificação formal baseada na Linguagem de Contratos Relativizada (RCL) e na ferramenta RECALL para modelar e detectar conflitos normativos em contratos multilaterais, antes da implementação em Solidity. A prova de conceito utiliza um contrato de compra e venda com quatro participantes, demonstrando que a versão original em RCL apresentava conflitos que impediam a entrega; uma versão corrigida, com uma nova cláusula de notificação de frete, resulta em um contrato sem conflitos e com fluxo completo quando implementado em Solidity e testado no Remix IDE. Os resultados destacam a importância da verificação formal no ciclo de desenvolvimento de contratos inteligentes e sugerem caminhos para automatizar a tradução de especificações formais para código Solidity, reforçando a segurança e auditabilidade de sistemas descentralizados.
Abstract
Smart contracts are tools with self-execution capabilities that provide enhanced security compared to traditional contracts; however, their immutability makes post-deployment fault correction extremely complex, highlighting the need for a verification layer prior to this stage. Although formalisms such as Contract Language (CL) enable logical analyses, they prove limited in attributing responsibilities within complex multilateral scenarios. This work presents a proof of concept using the Relativized Contract Language (RCL) and the RECALL tool for the specification and verification of a purchase and sale contract involving multiple agents. The study demonstrates the tool's capability to detect normative conflicts during the modeling phase. After correcting logical inconsistencies, the contract was translated into Solidity and functionally validated within the Remix IDE environment, confirming that prior formal verification is fundamental to ensuring the reliability and security of the final code.