Validating Solidity Code Defects using Symbolic and Concrete Execution powered by Large Language Models

Since the emergence of blockchain platforms like Ethereum [7], developers have implemented numerous Decentralized Applications (DApps) across diverse domains, from gaming to decentralized finance. Solidity [31] remains the most widely adopted programming language for the Ethereum ecosystem. However, like any emerging technology, this development paradigm introduced critical shortcomings. The impact of these defects is magnified by two of blockchain's core pillars: immutability, which historically prevented faulty code from being replaced, and public bytecode, which allows malicious actors to easily search for exploits. The devastating potential of such vulnerabilities was demonstrated by catastrophic events, including the "DAO Hack" [19] and the "Parity Wallet Hack" [23], which resulted in hundreds of millions of dollars in losses. The issues identified in Smart Contracts feature unique categories specific to the Blockchain environment. For instance, prominent examples include Reentrancy, a critical vulnerability where an external call allows an attacker's contract to repeatedly re-enter a function before its state has been updated, often leading to the complete draining of the contract's funds. Another distinct category involves Gas-Costly Patterns, which are not traditional security flaws but rather inefficient coding practices.