LLMs as verification oracles for Solidity

TL;DR

The paper systematically evaluates GPT-5 as a verification oracle for Solidity properties, constructing a large, ground-truth dataset of 2034 verification tasks across five contract use cases to compare LLM reasoning against formal tools SolCMC and Certora. It demonstrates that a reasoning-focused LLM can predict the validity of complex, contract-specific properties with high accuracy (GPT-5 ≈ $0.92$ F1 overall) and provide useful explanations and counterexamples, often outperforming traditional tools on tasks beyond their expressibility. The study also shows that LLMs can assist in real-world auditing scenarios, though challenges remain around spec alignment, numerical reasoning, and certifiability, highlighting a productive hybrid path where LLMs complement symbolic verification. Overall, the work argues for a practical convergence of AI and formal methods to improve secure smart-contract development and auditing, while outlining clear avenues to enhance reliability and coverage. The findings suggest that state-of-the-art LLMs can meaningfully accelerate auditing workflows when integrated with formal verification practices.

Abstract

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.