Uma Prova de Conceito para a Verificação Formal de Contratos Inteligentes
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866917214360174592 |
|---|---|
| author | Neves, Murilo de Souza Bonifacio, Adilson Luiz |
| author_facet | Neves, Murilo de Souza Bonifacio, Adilson Luiz |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2601_14427 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Uma Prova de Conceito para a Verificação Formal de Contratos Inteligentes Neves, Murilo de Souza Bonifacio, Adilson Luiz Cryptography and Security Logic in Computer Science Software Engineering 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. |
| title | Uma Prova de Conceito para a Verificação Formal de Contratos Inteligentes |
| topic | Cryptography and Security Logic in Computer Science Software Engineering |
| url | https://arxiv.org/abs/2601.14427 |