Smart contract vulnerabilities pose risks to decentralized finance (DeFi) ecosystems, with substantial financial losses from exploits. While large language models (LLMs) offer potential for security auditing, evaluation of prompting strategies and different models for vulnerability detection remains limited. We present a prompt engineering framework comparing seven different strategies (P0-P6) from zero-shot baselines to fine-tuned pipelines. Our prompt designs are implementations from high-performing methodologies: SmartGuard, GPTScan, LLM-SmartAudit, and iAudit. The framework supports evaluation across LLMs on the SmartBugs Curated benchmark with precision, recall, and F1 metrics. We provide: (1) a set of seven prompts (P0-P6) ranging from simple single questions to complex multi-agent and fine-tuned approaches, all producing results in the same JSON format for easy comparison; (2) a testing setup that measures how detection accuracy and API costs change as prompts get more complex; (3) open-source code with tools to run and score each prompt type automatically against any labeled smart contract dataset; and (4) a comparative study showing how each strategy performs on the SmartBugs Curated benchmark.
AI agents and institutional automation increasingly require public accountability, while many operational records must remain private due to personal data, trade secrets, contractual terms, security constraints, or audit boundaries. This paper introduces Two-Rail Verification, a public-private evidence-separation kernel for institutional AI and AI-agent governance. The proposed kernel distinguishes between a Public Rail, where public claims, status, version, timestamps, hashes, and verification routes can be placed, and a Private Rail, where raw records, personal data, cost structures, contracts, internal logs, secrets, and unpublished evidence remain protected. The contribution is not a new cryptographic primitive, a certification scheme, or a production assurance claim. Rather, Two-Rail organizes existing concepts such as hashes, signatures, manifests, verification kits, verifiable credentials, selective disclosure, zero-knowledge proofs, transparency logs, audit trails, and assurance reports into an institutional evidence-separation discipline. The kernel is expressed through four minimal requirements: cross-rail write prohibition, verified public claims, a verifiable public surface, and an accountability interface. The paper discusses the public-private evidence problem, adjacent technical and governance concepts, minimal public-surface design, use cases for AI agents and institutional records, and limitations. It does not claim third-party verification, complete signature coverage, legal compliance, safety guarantees, or an effective royalty-free patent pledge. Related patent applications may be pending, but any future patent pledge or license should be published separately with an effective date and stable URL.
This Article proposes a tripartite technical and legal framework designed to restore meaningful copyright enforcement in an era of large-scale generative artificial intelligence. The framework rests on three interlocking pillars. First, it mandates embedding of non-fungible token (NFT) provenance markers in all digitally published creative works, enabling immutable registration of every instance in which data is scraped or ingested by an AI system. Second, it establishes a compulsory labeling regime requiring that all AI-generated outputs carry a blockchain-anchored attestation of their machine origin and the training-data lineage that produced them. Third, it creates a royalty-settlement layer built on a purpose-designed stablecoin that triggers instantaneous, frictionless micropayments to rights holders whenever their content is used in AI training, inference, or downstream reproduction. The Article situates this proposal within the existing doctrinal architecture of U.S. copyright law, international treaty obligations, and emerging AI-governance legislation. It then subjects each pillar to rigorous technical scrutiny—examining blockchain throughput constraints, metadata-embedding standards, privacy-preserving attribution methods, and stablecoin monetary-policy design—before offering a unified statutory and regulatory roadmap for implementation.
Sara Migliorini, Mauro Gambini, Veronica Paternolli, Mila Dalla Preda
In the socio-economic landscape, we can recognize an emerging form of organization: the network coalition. A network coalition is a form of concerted cooperation in which a group of agents decides to collaborate to achieve a common goal. The decentralized and cooperative nature of a network coalition presents new challenges in automating its processes, which cannot be treated as traditional business processes managed by a centralized information system. In the literature, the notion of Exogenous Business Process (XBP) has been introduced to capture such processes. An XBP specification is intended as a potentially incomplete, renegotiable, procedural contract to which different parties adhere in order to achieve a predefined business goal. The concept of Enforceable Business Process (EBP) has been proposed as a possible abstraction for modeling and automating the XBPs of a network coalition. An EBP is essentially an evolution of the original concept of smart contract, which is able to properly manage contractual incompleteness while providing automatic enforceability. The aim of this paper is to formalize the notion of EBP and discuss how contractual incompleteness can be handled by a Decentralized Autonomous Information System (DAIS). The complete formalization of both procedural and incompleteness aspects of EBPs, as provided by this paper, lays the basis for the construction of the next generation of DAIS, as well as the diffusion of network coalition into many application domains, such as supply chains, business alliances, joint ventures, and others.
Abstract As we look to the future, how might decentralized autonomous organizations (DAOs) evolve? And where, beyond corporate law, might we find guidance for the legal questions those evolved DAOs pose? DAOs are, and will increasingly become, instrumentalities of artificial intelligence (AI). DAOs are connected with AI in at least three ways: They are tools for decentralized governance of AI data and models; AI may be used to automate the management and operations of DAOs; and DAOs themselves may function as a form of AI. As such, DAOs inherit the major regulatory and ethical challenges that AI poses, most notably with regard to autonomy. Thus, to consider the future questions DAOs pose and how to address them, we must look to the raging debates over AI regulation, and connect them to the more established themes of corporate law.
The immutable nature of smart contracts necessitates rigorous auditing, especially for ERC compliance, to prevent significant economic losses. While automated tools, particularly those combining Large Language Models (LLMs) with symbolic execution, have improved detection, they often suffer from false positives, false negatives, and insufficient interpretability. This paper introduces SymExplainer, a novel integrated framework designed to overcome these limitations. SymExplainer features an LLM-Enhanced Rule Semantic Extraction Module that deeply understands ERC specifications and misuse patterns using multi-stage prompting and a domain-specific knowledge base. Its Context-Aware Symbolic Execution Engine then efficiently prioritizes exploration paths based on these LLM insights. Crucially, a Violation Verification and Interpretability Generation Module performs secondary LLM-based cross-validation to significantly reduce false positives and produces comprehensive, natural language reports detailing "why," "where," and "how-to-fix" confirmed violations. Evaluated on a ground-truth dataset of 159 expert-annotated ERC violations, SymExplainer achieved perfect recall with zero false negatives and substantially reduced false positives to only 15, outperforming state-of-the-art methods like SymGPT (which reported 29 false positives and 1 false negative). An ablation study confirmed the critical contribution of each module, and qualitative human evaluation validated the high clarity, accuracy, and actionability of its interpretability reports. Despite a modest increase in computational cost, SymExplainer provides a more precise, reliable, and transparent solution for smart contract auditing through unparalleled accuracy, reduced noise, and actionable insights.
Oscar Medina, Brenda Meloni, Ana Strub, Marelo Martín Marciszack
Event patterns are used to model interactions between smart contracts and their environment, improving the efficiency, security, and flexibility of applications based on blockchain technologies. Event pattern-driven smart contract modelling is an emerging trend. Defining a new pattern or selecting a pre-existing one from a limited catalog is a fundamental activity for any analysis model that utilizes event patterns. This study presents a proposal to manage a catalog of event patterns that can be applied to the conceptual modelling of smart contracts and incorporates machine learning techniques to optimize pattern selection. To test this proposal, a prototype application called PatCat (Pattern Catalogue) was developed, using a decentralized electronic voting application as a case study. The incorporation of patterns at the beginning of the modelling process simplifies and clarifies the elicitation of requirements, among other benefits, while the use of machine learning accelerates the description of the problem situation. Consequently, a specialized application for managing a catalog of event patterns, supported by machine learning techniques, proves useful in standardizing and streamlining smart contract modelling tasks.
Abdul Aziz Usman Balarabe, Gilbert I.O. Aimufua, Kene Tochukwu Anyachebelu, Umar Abdullahi
The management of judicial workflow through traditional paper-based and centralized systems presents a wide range of challenges. This is particularly evident in processes such as: case filing, evidence submission, and verdict execution, where inefficiencies, bureaucratic delays, and security vulnerabilities often undermine the credibility of the judiciary. While electronic systems like Case Management Systems (CMS) and Electronic Court Filing (ECF) have been introduced to digitize court operations, they remain largely centralized and therefore susceptible to unauthorized access, data manipulation, and cyberattacks. Numerous scholars have proposed digital and automated solutions for judicial processes; however, existing models often fail to adequately address key challenges of transparency, immutability, and interoperability across jurisdictions. The main objective of this paper is to provide a blockchain-enabled smart contract framework for judicial workflow management that integrates automation, security, and transparency into legal processes. Data flow and use case diagrams were developed to illustrate the core functionalities of the framework, including case registration, evidence management, judicial rulings, and court scheduling. Access to records within the framework is governed by blockchain’s decentralized consensus mechanism, while smart contracts automate routine judicial tasks based on predefined rules. The adoption of this approach is expected to significantly reduce administrative inefficiencies, minimize fraudulent practices, and enhance trust in judicial outcomes.
A revolução tecnológica está transformando profundamente a sociedade, alterando a forma como nos organizamos politicamente e nos inserimos no tempo e no espaço. A introdução de novas tecnologias, no campo das contratações, tem propiciado, no âmbito privado, reflexões importantes sobre a possibilidade de utilizar a inteligência artificial e os smart contracts para resolver problemas como a incompletude contratual e o descumprimento de obrigações. O artigo tem por finalidade descrever como esse processo vem se desenvolvendo e avaliar a possibilidade de incorporar esses novos instrumentos às contratações públicas brasileiras, considerando as regras jurídicas aplicáveis a esse tipo de relação e as particularidades do arranjo institucional nacional.
The rapid digitization of commercial, governmental, and legal transactions has created an urgent need for efficient, secure, and transparent dispute resolution mechanisms. Traditional arbitration systems often fall short when handling the complexity and volume of digital evidence, smart contracts, and cross-border interactions. This study proposes a novel AI-powered digital arbitration framework that integrates smart contracts, blockchain-based evidence authentication, and explainable artificial intelligence (AI) to automate and modernize the arbitration process. The framework comprises three core layers: (i) a smart contract-based agreement layer that encodes legal terms and self-executing arbitration clauses; (ii) a blockchain-based evidence management layer that ensures the integrity, authenticity, and traceability of submitted evidence; and (iii) an AI-based arbitration engine that classifies, interprets, and evaluates evidence using transformer and LSTM models, supported by SHAP and LIME for interpretability. A controlled experimental setup was implemented using Ethereum and Hyperledger Fabric testnets, with AI models trained on 1,200 annotated arbitration cases. Results demonstrate a 99.5% reduction in arbitration time, a 92.4% agreement rate between AI and expert rulings, and a 99% accuracy in tampering detection. Furthermore, 87.3% of AI-generated decisions were rated as interpretable and acceptable by legal experts. These findings confirm the system's ability to deliver fast, accurate, and explainable arbitration decisions while complying with legal standards. This research contributes a foundational blueprint for deploying autonomous arbitration systems in digital governance, offering scalable solutions for future applications in smart contracts, e-commerce disputes, and algorithmic legal infrastructure.
Eranga Bandara, Sachin Shetty, Ravi Mukkamala, Ross Gore · 12 authors
In recent years, blockchain has experienced widespread adoption across various industries, becoming integral to numerous enterprise applications. Concurrently, the rise of generative AI and LLMs has transformed human-computer interactions, offering advanced capabilities in understanding and generating human-like text. The introduction of the MCP has further enhanced AI integration by standardizing communication between AI systems and external data sources. Despite these advancements, there is still no standardized method for seamlessly integrating LLM applications and blockchain. To address this concern, we propose "MCC: Model Context Contracts" a novel framework that enables LLMs to interact directly with blockchain smart contracts through MCP-like protocol. This integration allows AI agents to invoke blockchain smart contracts, facilitating more dynamic and context-aware interactions between users and blockchain networks. Essentially, it empowers users to interact with blockchain systems and perform transactions using queries in natural language. Within this proposed architecture, blockchain smart contracts can function as intelligent agents capable of recognizing user input in natural language and executing the corresponding transactions. To ensure that the LLM accurately interprets natural language inputs and maps them to the appropriate MCP functions, the LLM was fine-tuned using a custom dataset comprising user inputs paired with their corresponding MCP server functions. This fine-tuning process significantly improved the platform's performance and accuracy. To validate the effectiveness of MCC, we have developed an end-to-end prototype implemented on the Rahasak blockchain with the fine-tuned Llama-4 LLM. To the best of our knowledge, this research represents the first approach to using the concept of Model Context Protocol to integrate LLMs with blockchain.
سازمانهای خودگردان غیرمتمرکز (DAO)، به دلیل ویژگیهایی چون فقدان مدیریت انسانی متمرکز و ساختار فراملی، با مفهوم سنتی شخصیت حقوقی در تضاد ماهوی قرار دارند. پژوهش حاضر از توصیف این بنبست شناختهشده عبور کرده و به یک پرسش راهبردی پاسخ میدهد: نظام حقوقی ایران چگونه میتواند با الهام از مبانی فقهی و تحلیل تطبیقی تجارب نوین جهانی (مانند وایومینگ)، مدلی جدید تحت عنوان «شخصیت حقوقی الگوریتمی» را طراحی و شناسایی کند؟ این تحقیق با روش توصیفی-تحلیلی، پس از اثبات ناکارآمدی چارچوبهای فعلی برای حل بحران مسئولیت و صلاحیت قضایی، به عنوان یافته اصلی، ارکان و الزامات یک مدل مفهومی نوین را ارائه میدهد. این مدل، اهلیت و موجودیت نهاد را نه بر ارکان انسانی، بلکه بر شفافیت کد، قابلیت حسابرسی الگوریتم و معرفی یک عامل ثبتشده استوار میسازد. مقاله همچنین با بررسی تطبیقی رویکردهای جهانی و پاسخگویی به انتقادات کلیدی، اعتبار و کارآمدی مدل پیشنهادی را تقویت مینماید. نتیجهگیری پژوهش آن است که مواجهه کارآمد با DAO مستلزم عبور از راهکارهای اصلاحی و حرکت به سمت قانونگذاری جدید و ویژهای است که این شخصیت حقوقی فناورانه را به رسمیت بشناسد و ضمن فراهم آوردن بستر نوآوری اقتصادی، پاسخگویی حقوقی و قضایی این نهادها را در برابر حاکمیت تضمین نماید.
Smart contracts are central to blockchain ecosystems, yet their development remains technically demanding, error-prone, and tied to platform-specific programming languages. This paper introduces SCEditor-Web, a web-based modeling environment that combines model-driven engineering (MDE) with generative artificial intelligence (Gen-AI) to simplify contract design and code generation. Developers specify the structural and behavioral aspects of smart contracts through a domain-specific visual language grounded in a formal metamodel. The resulting contract model is exported as structured JSON and transformed into executable, platform-specific code using large language models (LLMs) guided by a tailored prompt engineering process. A prototype implementation was evaluated on Solidity contracts as a proof of concept, using representative use cases. Experiments with state-of-the-art LLMs assessed the generated contracts for compilability, semantic alignment with the contract model, and overall code quality. Results indicate that the visual-to-code workflow reduces manual effort, mitigates common programming errors, and supports developers with varying levels of expertise. The contributions include an abstract smart contract metamodel, a structured prompt generation pipeline, and a web-based platform that bridges high-level modeling with practical multi-language code synthesis. Together, these elements advance the integration of MDE and LLMs, demonstrating a step toward more accessible and reliable smart contract engineering.
Ye Li, Mengliang Li, Dehai Zhao, Jiamou Sun · 5 authors
Solidity, the dominant smart contract language for Ethereum, has rapidly evolved with frequent version updates to enhance security, functionality, and developer experience. However, these continual changes introduce significant challenges, particularly in compilation errors, code migration, and maintenance. Therefore, we conduct an empirical study to investigate the challenges in the Solidity version evolution and reveal that 81.68 % of examined contracts encounter errors when compiled across different versions, with 86.92 % of compilation errors. To mitigate these challenges, we conducted a systematic evaluation of large language models (LLMs) for resolving Solidity compilation errors during version migrations. Our empirical analysis across both open-source (LLaMA3, DeepSeek) and closedsource (GPT-4o, GPT-3.5-turbo) LLMs reveals that although these models exhibit error repair capabilities, their effectiveness diminishes significantly for semantic-level issues and shows strong dependency on prompt engineering strategies. This underscores the critical need for domain-specific adaptation in developing reliable LLM-based repair systems for smart contracts. Building upon these insights, we introduce SMCFIXER, a novel framework that systematically integrates expert knowledge retrieval with LLM-based repair mechanisms for Solidity compilation error resolution. The architecture comprises three core phases: (1) context-aware code slicing that extracts relevant error information; (2) expert knowledge retrieval from official documentation; and (3) iterative patch generation for Solidity migration. Experimental validation across Solidity version migrations demonstrates our approach's statistically significant 24.24% improvement over baseline GPT-4o on real-world datasets, achieving near-perfect 96.97% accuracy.
Widespread reuse of open-source code in smart contract development boosts programming efficiency but significantly amplifies bug propagation across contracts, while dedicated methods for detecting similar smart contract functions remain very limited. Conventional abstract-syntax-tree (AST) based methods for smart contract similarity detection face challenges in handling intricate tree structures, which impedes detailed semantic comparison of code. Recent deep-learning based approaches tend to overlook code syntax and detection interpretability, resulting in suboptimal performance. To fill this research gap, we introduce SmartDetector, a novel approach for computing similarity between smart contract functions, explainable at the fine-grained statement level. Technically, SmartDetector decomposes the AST of a smart contract function into a series of smaller statement trees, each reflecting a structural element of the source code. Then, SmartDetector uses a classifier to compute the similarity score of two functions by comparing each pair of their statement trees. To address the infinite hyperparameter space of the classifier, we mathematically derive a cosine-wise diffusion process to efficiently search optimal hyperparameters. Extensive experiments conducted on three large real-world datasets demonstrate that SmartDetector outperforms current state-of-the-art methods by an average improvement of 14.01% in F1-score, achieving an overall average F1-score of 95.88%.
Smart contracts play a pivotal role in blockchain ecosystems, and fuzzing remains a critical approach to securing them. However, existing smart contract fuzzers often optimize either seed generation or mutation scheduling in isolation and rely on narrow, fragmented feedback signals, leaving multi-transaction reasoning and stagnation recovery under-explored. In this work, we propose aLarge Language Models(LLMs)-based Multi-feedback Smart Contract Fuzzing framework (LLAMA). Key components of the proposed LLAMA include: (i) a hierarchical prompting strategy that guides LLMs to generate structurally valid, context-aware multi-transaction initial seeds, together with a lightweight pre-fuzzing phase that validates and prioritizes high-potential LLM-generated candidates; (ii) a multi-feedback-guided evolutionary optimization module that jointly optimizes seed selection and mutation scheduling by a group of constraints for driving an LLM-bootstrapped bandit scheduler. (iii) an LLM-guided hybrid fuzzing module that integrates evolutionary fuzzing with a dual-channel recovery mechanism, which concurrently employs asynchronous coverage-stagnation- based LLM reseeding and selective symbolic execution to resolve complex path constraints. Our extensive experiments demonstrate that LLAMA outperforms state-of-the-art fuzzers in both coverage and vulnerability detection. Specifically, it achieves 92% instruction coverage on small contracts and 81% on large contracts, while detecting 132 out of 148 known vulnerabilities across diverse categories. Ablation studies further evidence that the proposed multi-feedback and hybrid recovery strategies have strong impact on LLAMA’s performance. The results explain LLAMA’s effectiveness, adaptability, and practicality in complex smart contract scenarios.
The emergence of the Metaverse as a decentralized digital ecosystem has transformed traditional contract enforcement by introducing smart contracts, self-executing agreements embedded in blockchain systems. This study conducts a comparative legal analysis of the regulatory frameworks governing smart contracts within Metaverse operations in Nigeria and Uganda. Employing a doctrinal legal method, the research critically examines primary legal sources such as statutory laws and case law, alongside scholarly literature, to assess legal recognition, enforceability, and institutional preparedness. The study reveals a significant regulatory gap in Nigeria, where the absence of a comprehensive legal framework creates uncertainty in the enforceability of smart contracts, despite growing blockchain policy initiatives. In contrast, Uganda has established more definitive legal provisions, particularly through its Electronic Transactions and Signature Acts, which explicitly validate digital contracts. The novelty of this study lies in its regional comparative focus on emerging economies and its analysis of how traditional contract principles interact with decentralized digital platforms. The urgency of this inquiry is underscored by the rapid digitalization of commerce, which necessitates timely legal adaptation to prevent regulatory obsolescence and safeguard stakeholders. This research contributes to the discourse on digital governance by proposing a legal reform agenda for Nigeria, advocating for the adoption of a smart contract-enabling framework modeled after Uganda’s approach. Ultimately, it calls for regional and international harmonization to ensure legal certainty, consumer protection, and dispute resolution within Metaverse-driven economies.
Jishnu Patlola, Rishitha Manyam, Himakar Chappidi, K Suvarchala
This paper investigates the application of CodeBERT, a pre-trained transformer model, to improve the detection of vulnerabilities in smart contracts.Smart contracts, while central to blockchain technology, are susceptible to security flaws that can result in significant financial and operational risks.By fine-tuning CodeBERT on labeled datasets specifically curated for smart contracts, our approach enhances the precision and efficiency of identifying various security issues.This method not only offers a robust solution to the existing challenges in blockchain security but also contributes to the broader efforts to secure decentralized systems and ensure the reliability of blockchain applications
Smart contracts, closely intertwined with cryptocurrency transactions, have sparked widespread concerns about considerable financial losses of security issues. To counteract this, a variety of tools have been developed to identify vulnerability in smart contract. However, they fail to overcome two challenges at the same time when faced with smart contract bytecode: (i) strong interference caused by enormous non-relevant instructions; (ii) missing semantics of bytecode due to incomplete data and control flow dependencies. In this paper, we propose a multi-teacher based bytecode vulnerability detection method, namely Multi-Teacher Vulnerability Hunter (MTVHunter), which delivers effective denoising and missing semantic to bytecode under multi-teacher guidance. Specifically, we first propose an instruction denoising teacher to eliminate noise interference by abstract vulnerability pattern and further reflect in contract embeddings. Secondly, we design a novel semantic complementary teacher with neuron distillation, which effectively extracts necessary semantic from source code to replenish the bytecode. Particularly, the proposed neuron distillation accelerate this semantic filling by turning the knowledge transition into a regression task. We conduct experiments on 229,178 real-world smart contracts that concerns four types of common vulnerabilities. Extensive experiments show MTVHunter achieves significantly performance gains over state-of-the-art approaches.
Semantic code search technology allows searching for existing code snippets through natural language, which can greatly improve programming efficiency. Smart contracts, programs that run on the blockchain, have a code reuse rate of more than 79%, which means developers have a great demand for semantic code search tools. However, the existing code search models still have a semantic gap between code and query and perform poorly on specialized queries of smart contracts. In this paper, we propose a Multi-Modal Smart contract Code Search (MM-SCS) model. Specifically, we construct a Contract Elements Dependency Graph (CEDG) for MM-SCS as an additional modality to capture the data flow and control flow information of the code. To make the model more focused on the key contextual information, we use a multi-head attention network to generate embeddings for code features. In addition, we use a fine-tuned pretrained model to ensure the model's effectiveness when the training data is small. We compared MM-SCS with four state-of-the-art models on a dataset with 470K (code, docstring) pairs collected from Github and Etherscan. Experimental results show that MM-SCS achieves an MRR (Mean Reciprocal Rank) of 0.572, outperforming four state-of-the-art models UNIF, DeepCS, CARLCS-CNN, and TAB-CS by 34.2%, 59.3%, 36.8%, and 14.1%, respectively. Additionally, the search speed of MM-SCS is second only to UNIF, reaching 0.34s/query.
This study investigates the transformative impact of digitization on legal systems in developing countries, emphasizing the integration of emerging technologies such as blockchain and smart contracts. By exploring case studies from India, Kenya, Brazil, Rwanda, South Africa, the Philippines, and Ghana, the research highlights how digital adoption enhances legal infrastructure, expands access to justice, and drives regulatory evolution. A mixed-method approach, combining qualitative interviews and quantitative analysis of legal reforms, reveals that digitization significantly reduces case backlogs, improves transparency, and accelerates judicial processes. However, persistent challenges, including inadequate digital infrastructure, disparities in digital literacy, and cybersecurity vulnerabilities, underscore the need for coordinated interventions. The study identifies blockchain as a critical tool for ensuring the integrity and security of legal records, providing tamper-proof documentation, and fostering trust in legal processes. Similarly, smart contracts streamline legal transactions by automating and enforcing agreements, reducing costs, and enhancing efficiency. These technologies are essential for modernizing judicial frameworks and addressing governance gaps, particularly in regions grappling with corruption and bureaucratic inefficiencies. Ultimately, the findings underscore the importance of phased implementation strategies, investments in digital literacy, and inclusive policy frameworks to maximize the benefits of legal digitization. By integrating blockchain and smart contracts, developing countries can build resilient, transparent, and accessible legal systems that respond to the dynamic needs of their societies.
Jan Corazza, Ivan Gavran, Gabriela Moreira, Daniel Neider
When blockchain systems are said to be trustless, what this really means is that all the trust is put into software. Thus, there are strong incentives to ensure blockchain software is correct -- vulnerabilities here cost millions and break businesses. One of the most powerful ways of establishing software correctness is by using formal methods. Approaches based on formal methods, however, induce a significant overhead in terms of time and expertise required to successfully employ them. Our work addresses this critical disadvantage by automating the creation of a formal model -- a mathematical abstraction of the software system -- which is often a core task when employing formal methods. We perform model synthesis in three phases: we first transpile the code into model stubs; then we "fill in the blanks" using a large language model (LLM); finally, we iteratively repair the generated model, on both syntactical and semantical level. In this way, we significantly reduce the amount of time necessary to create formal models and increase accessibility of valuable software verification methods that rely on them. The practical context of our work was reducing the time-to-value of using formal models for correctness audits of smart contracts.