Uma Prova de Conceito para a Verifica\c{c}\~ao Formal de Contratos Inteligentes

TL;DR

This paper demonstrates a proof of concept using RCL and RECALL for formal verification of smart contracts, highlighting the importance of pre-deployment analysis to ensure security and correctness.

Contribution

It introduces a novel approach combining RCL and RECALL for formal specification and verification of multi-agent smart contracts, addressing limitations of existing formalisms.

Findings

Detection of normative conflicts during modeling

Successful translation and validation in Solidity

Verification improves contract reliability and security

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.