Recent large language models (LLMs) incorporate reasoning capabilities that allow them to perform well in predicting whether a smart contract respects a certain property, suggesting a complementary approach to traditional formal-methods-based techniques for smart contract verification. However, the application of LLMs in such context has two major issues: 1) properties expressed in natural language are intrinsically ambiguous, and 2) answers returned by LLMs have no guarantee of correctness. In this paper, we address both issues simultaneously by: 1) introducing a new formal specification language that extends Solidity with abstract types, and 2) designing a workflow that combines LLMs with type checking and concrete execution to generate and validate violation witnesses (i.e., counterexamples). The key idea is to represent a specification as a Solidity test with (existentially quantified) variables of abstract type; finding an instantiation of these variables to concrete values (of the correct type) concretizes the test into an executable counterexample (PoC) for the target property. We implemented our procedure in the tool Neuroforger, experimentally evaluating it on a smart-contract verification dataset drawn from literature, obtaining promising results that demonstrate its potential applicability in the wild.

翻译：近期的大语言模型（LLMs）融入了推理能力，使其在预测智能合约是否遵守特定属性方面表现出色，这为传统的基于形式化方法的智能合约验证技术提供了补充性思路。然而，在此类场景中应用LLMs存在两大主要问题：1）以自然语言表达的属性本质上具有歧义性；2）LLMs返回的结果无法保证正确性。本文通过以下方式同时解决这两个问题：1）引入一种新的形式化规范语言，该语言通过抽象类型扩展了Solidity；2）设计一种将LLMs与类型检查和具体执行相结合的流程，用于生成并验证违规证据（即反例）。其核心思想是将规范表示为带有（存在量词约束的）抽象类型变量的Solidity测试用例；通过对这些变量进行具体值（符合正确类型）的实例化，可将该测试用例转化为针对目标属性的可执行反例（PoC）。我们在工具Neuroforger中实现了该流程，并基于来自文献的智能合约验证数据集进行实验评估，获得了验证其实际应用潜力的初步成果。