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.

翻译：智能合约是具有自动执行能力的工具，相较于传统合约提供了更高的安全性；然而，其不可变性使得部署后故障修复变得极其复杂，这凸显了在此阶段之前建立验证层的必要性。尽管契约语言（CL）等形式化方法支持逻辑分析，但在复杂的多边场景中分配责任方面仍存在局限性。本研究提出了一种使用相对化契约语言（RCL）和RECALL工具进行多主体买卖合约规约与验证的概念验证。该研究展示了该工具在建模阶段检测规范冲突的能力。在修正逻辑不一致性后，合约被转换为Solidity语言，并在Remix IDE环境中进行了功能验证，证实了先期形式化验证对于确保最终代码的可靠性与安全性具有基础性作用。