Smart Contracts Formal Verification: A Systematic Literature Review
- URL: http://arxiv.org/abs/2510.17865v1
- Date: Wed, 15 Oct 2025 21:32:57 GMT
- Title: Smart Contracts Formal Verification: A Systematic Literature Review
- Authors: Rene Davila, Everardo Barcenas, Rocio Aldeco-Perez,
- Abstract summary: Formal verification entails testing software to ensure it operates as specified.<n>Smart Contracts, as software models, often contain notable errors in their operation or specifications.<n>This survey proposes an alternative formal verification based on description logic.
- Score: 0.0
- License: http://creativecommons.org/publicdomain/zero/1.0/
- Abstract: Formal verification entails testing software to ensure it operates as specified. Smart contracts are self-executing contracts with the terms of the agreement directly written into lines of code. They run on blockchain platforms and automatically enforce and execute the terms of an agreement when meeting predefined conditions. However, Smart Contracts, as software models, often contain notable errors in their operation or specifications. This observation prompts us to conduct a focused study examining related works published across various sources. These publications detail specifications, verification tools, and relevant experiments. Subsequently, this survey proposes an alternative formal verification based on description logic.
Related papers
- Uma Prova de Conceito para a Verificação Formal de Contratos Inteligentes [0.0]
This work presents a proof of concept using the Relativized Contract Language (RCL) and the RECALL tool.<n>The study demonstrates the tool's capability to detect normative conflicts during the modeling phase.
arXiv Detail & Related papers (2026-01-20T19:38:17Z) - Validation Framework for E-Contract and Smart Contract [0.6312266245317322]
We propose and develop a framework for validating smart contracts derived from e-contracts.<n>The proposed framework will systematically compare and validate the terms and clauses of the e-contracts with the logic of the smart contracts.<n>This validation confirms that the agreement is accurately translated into executable code.
arXiv Detail & Related papers (2025-04-27T07:23:46Z) - SolBench: A Dataset and Benchmark for Evaluating Functional Correctness in Solidity Code Completion and Repair [51.0686873716938]
We introduce SolBench, a benchmark for evaluating the functional correctness of Solidity smart contracts generated by code completion models.<n>We propose a Retrieval-Augmented Code Repair framework to verify functional correctness of smart contracts.<n>Results show that code repair and retrieval techniques effectively enhance the correctness of smart contract completion while reducing computational costs.
arXiv Detail & Related papers (2025-03-03T01:55:20Z) - Vulnerabilities of smart contracts and mitigation schemes: A Comprehensive Survey [0.6554326244334866]
This paper presents a literature review combined with an experimental report that aims to assist developers in developing secure smarts.
It provides a list of frequent vulnerabilities and corresponding mitigation solutions.
It evaluates the community most widely used tools by executing and testing them on sample smart contracts.
arXiv Detail & Related papers (2024-03-28T19:36:53Z) - Specification Mining for Smart Contracts with Trace Slicing and Predicate Abstraction [10.723903783651537]
We propose a specification mining approach to infer contract specifications from past transaction histories.<n>Our approach derives high-level behavioral automata of function invocations, accompanied by program invariants statistically inferred from the transaction histories.<n>Experiments show that SMCON mines reasonably accurate specifications that can be used to enhance symbolic analysis of smart contracts achieving higher code coverage and up to 56% speedup.
arXiv Detail & Related papers (2024-03-20T03:39:51Z) - Contract Usage and Evolution in Android Mobile Applications [45.44831696628473]
We present the first large-scale empirical study on the presence and use of contracts in Android applications, written in Java or Kotlin.
We analyzed 2,390 Android applications from the F-Droid repository and processed more than 51,749 KLOC.
Our findings show that it would be desirable to have libraries that standardize contract specifications in Java and Kotlin.
arXiv Detail & Related papers (2024-01-25T15:36:49Z) - Formally Verifying a Real World Smart Contract [52.30656867727018]
We search for a tool capable of formally verifying a real-world smart contract written in a recent version of Solidity.
In this article, we present our search for a tool capable of formally verifying a real-world smart contract written in a recent version of Solidity.
arXiv Detail & Related papers (2023-07-05T14:30:21Z) - Lessons from Formally Verified Deployed Software Systems (Extended version) [65.69802414600832]
This article examines a range of projects, in various application areas, that have produced formally verified systems and deployed them for actual use.
It considers the technologies used, the form of verification applied, the results obtained, and the lessons that the software industry should draw regarding its ability to benefit from formal verification techniques and tools.
arXiv Detail & Related papers (2023-01-05T18:18:46Z) - ConReader: Exploring Implicit Relations in Contracts for Contract Clause
Extraction [84.0634340572349]
We study automatic Contract Clause Extraction (CCE) by modeling implicit relations in legal contracts.
In this work, we first comprehensively analyze the complexity issues of contracts and distill out three implicit relations commonly found in contracts.
We propose a novel framework ConReader to exploit the above three relations for better contract understanding and improving CCE.
arXiv Detail & Related papers (2022-10-17T02:15:18Z) - Detecting Logical Relation In Contract Clauses [94.85352502638081]
We develop an approach to automate the extraction of logical relations between clauses in a contract.
The resulting approach should help contract authors detecting potential logical conflicts between clauses.
arXiv Detail & Related papers (2021-11-02T19:26:32Z)
This list is automatically generated from the titles and abstracts of the papers in this site.
This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.