# A Survey of Smart Contract Formal Specification and Verification

arXiv: https://arxiv.org/abs/2008.02712 · HTML: https://mlsanity.com/paper/2008.02712/

## Key facts

- Cited by 14 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 6 Aug 2020.

## Built on by (most cited first, 14 of 14)

- [PropertyGPT: LLM-driven Formal Verification of Smart Contracts through Retrieval-Augmented Property Generation](https://mlsanity.com/paper/2405.02580/) (2024)
- [Prompt to Pwn: Automated Exploit Generation for Smart Contracts](https://mlsanity.com/paper/2508.01371/) (2025)
- [Vulnerability Detection in Ethereum Smart Contracts via Machine Learning: A Qualitative Analysis](https://mlsanity.com/paper/2407.18639/) (2024)
- [CodeBC: A More Secure Large Language Model for Smart Contract Code Generation in Blockchain](https://mlsanity.com/paper/2504.21043/) (2025)
- [Adaptive Plan-Execute Framework for Smart Contract Security Auditing](https://mlsanity.com/paper/2505.15242/) (2025)
- [Movement Analytics: Current Status, Application to Manufacturing, and Future Prospects from an AI Perspective](https://mlsanity.com/paper/2210.01344/) (2022)
- [FTSmartAudit: A Knowledge Distillation-Enhanced Framework for Automated Smart Contract Auditing Using Fine-Tuned LLMs](https://mlsanity.com/paper/2410.13918/) (2024)
- [UEChecker: Detecting Unchecked External Call Vulnerabilities in DApps via Graph Analysis](https://mlsanity.com/paper/2508.01343/) (2025)
- [Discounting in Strategy Logic](https://mlsanity.com/paper/2305.15256/) (2023)
- [A Survey on Blockchain-based Supply Chain Finance with Progress and Future directions](https://mlsanity.com/paper/2408.08915/) (2024)
- [Logical foundations of Smart Contracts](https://mlsanity.com/paper/2502.09232/) (2025)
- [Towards Understanding Deep Learning Model in Image Recognition via Coverage Test](https://mlsanity.com/paper/2505.08814/) (2025)
- [LLMs as verification oracles for Solidity](https://mlsanity.com/paper/2509.19153/) (2025)
- [DMind-3: A Sovereign Edge--Local--Cloud AI System with Controlled Deliberation and Correction-Based Tuning for Safe, Low-Latency Transaction Execution](https://mlsanity.com/paper/2602.11651/) (2026)

## Abstract (arXiv)

A smart contract is a computer program which allows users to automate their actions on the blockchain platform. Given the significance of smart contracts in supporting important activities across industry sectors including supply chain, finance, legal and medical services, there is a strong demand for verification and validation techniques. Yet, the vast majority of smart contracts lack any kind of formal specification, which is essential for establishing their correctness. In this survey, we investigate formal models and specifications of smart contracts presented in the literature and present a systematic overview in order to understand the common trends. We also discuss the current approaches used in verifying such property specifications and identify gaps with the hope to recognize promising directions for future work.