Neuroforger: certified violation witnesses for smart contracts verification via LLMs
This work provides a new method for smart contract developers to verify properties and find counterexamples, addressing the limitations of LLMs in this domain.
This paper tackles the problem of verifying smart contracts using LLMs by addressing the ambiguity of natural language properties and the lack of correctness guarantees from LLMs. They introduce a formal specification language and a workflow combining LLMs with type checking and concrete execution to generate and validate violation witnesses.
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.