# LLMs as verification oracles for Solidity

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 21 of its 55 references that are in the map.
- First posted on arXiv 23 Sep 2025.

## Builds on (most cited first, 21 of 21)

- [Language Models are Few-Shot Learners](https://mlsanity.com/paper/2005.14165/) (2020)
- [Chain-of-Thought Prompting Elicits Reasoning in Large Language Models](https://mlsanity.com/paper/2201.11903/) (2022)
- [Large Language Models are Zero-Shot Reasoners](https://mlsanity.com/paper/2205.11916/) (2022)
- [Evaluating the Logical Reasoning Ability of ChatGPT and GPT-4](https://mlsanity.com/paper/2304.03439/) (2023)
- [A New Era in Software Security: Towards Self-Healing Software via Large Language Models and Formal Verification](https://mlsanity.com/paper/2305.14752/) (2023)
- [PropertyGPT: LLM-driven Formal Verification of Smart Contracts through Retrieval-Augmented Property Generation](https://mlsanity.com/paper/2405.02580/) (2024)
- [Do you still need a manual smart contract audit?](https://mlsanity.com/paper/2306.12338/) (2023)
- [Proof Automation with Large Language Models](https://mlsanity.com/paper/2409.14274/) (2024)
- [How Effective are Smart Contract Analysis Tools? Evaluating Smart Contract Static Analysis Tools Using Bug Injection](https://mlsanity.com/paper/2005.11613/) (2020)
- [From Informal to Formal -- Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs](https://mlsanity.com/paper/2501.16207/) (2025)
- [A Survey of Smart Contract Formal Specification and Verification](https://mlsanity.com/paper/2008.02712/) (2020)
- [AI Agent Smart Contract Exploit Generation](https://mlsanity.com/paper/2507.05558/) (2025)
- [solc-verify: A Modular Verifier for Solidity Smart Contracts](https://mlsanity.com/paper/1907.04262/) (2019)
- [Clockwork Finance: Automated Analysis of Economic Security in Smart Contracts](https://mlsanity.com/paper/2109.04347/) (2021)
- [Prompt to Pwn: Automated Exploit Generation for Smart Contracts](https://mlsanity.com/paper/2508.01371/) (2025)
- [Zero-Collateral Lotteries in Bitcoin and Ethereum](https://mlsanity.com/paper/1612.05390/) (2016)
- [Quantitative Analysis of Smart Contracts](https://mlsanity.com/paper/1801.03367/) (2018)
- [Towards benchmarking of Solidity verification tools](https://mlsanity.com/paper/2402.10750/) (2024)
- [Solvent: liquidity verification of smart contracts](https://mlsanity.com/paper/2404.17864/) (2024)
- [Formal verification in Solidity and Move: insights from a comparative analysis](https://mlsanity.com/paper/2502.13929/) (2025)
- [A theory of Lending Protocols in DeFi](https://mlsanity.com/paper/2506.15295/) (2025)

## Abstract (arXiv)

Ensuring the correctness of smart contracts is critical, as even subtle flaws can lead to severe financial losses. While bug detection tools able to spot common vulnerability patterns can serve as a first line of defense, most real-world exploits and losses stem from errors in the contract business logic. Formal verification tools such as SolCMC and the Certora Prover address this challenge, but their impact remains limited by steep learning curves and restricted specification languages. Recent works have begun to explore the use of large language models (LLMs) for security-related tasks such as vulnerability detection and test generation. Yet, a fundamental question remains open: can LLMs aid in assessing the validity of arbitrary contract-specific properties? In this paper, we provide the first systematic empirical evaluation of GPT-5, a state-of-the-art reasoning LLM, in this role. We benchmark its performance on a large dataset of verification tasks, compare its outputs against those of established formal verification tools, and assess its practical effectiveness in real-world auditing scenarios. Our study combines quantitative metrics with qualitative analysis, and shows that recent reasoning-oriented LLMs - although lacking soundness guarantees - can be surprisingly effective at predicting the (in)validity of complex properties, suggesting a new frontier in the convergence of AI and formal methods for secure smart contract development and auditing.