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 serve as verification oracles, capable of reasoning
about arbitrary contract-specific properties? In this paper, we provide the
first systematic 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 can be surprisingly effective as verification oracles,
suggesting a new frontier in the convergence of AI and formal methods for
secure smart contract development and auditing.