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

arXiv: https://arxiv.org/abs/2509.13023 · HTML: https://mlsanity.com/paper/2509.13023/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 13 of its 37 references that are in the map.
- First posted on arXiv 16 Sep 2025.

## Builds on (most cited first, 13 of 13)

- [LLaMA: Open and Efficient Foundation Language Models](https://mlsanity.com/paper/2302.13971/) (2023)
- [DeepSeek-R1: Incentivizing Reasoning Capability in LLMs via Reinforcement Learning](https://mlsanity.com/paper/2501.12948/) (2025)
- [Gemini 1.5: Unlocking multimodal understanding across millions of tokens of context](https://mlsanity.com/paper/2403.05530/) (2024)
- [IRIS: LLM-Assisted Static Analysis for Detecting Security Vulnerabilities](https://mlsanity.com/paper/2405.17238/) (2024)
- [Slither: A Static Analysis Framework For Smart Contracts](https://mlsanity.com/paper/1908.09878/) (2019)
- [Securify: Practical Security Analysis of Smart Contracts](https://mlsanity.com/paper/1806.01143/) (2018)
- [When ChatGPT Meets Smart Contract Vulnerability Detection: How Far Are We?](https://mlsanity.com/paper/2309.05520/) (2023)
- [A Survey of Symbolic Execution Techniques](https://mlsanity.com/paper/1610.00502/) (2016)
- [LLM-SmartAudit: Advanced Smart Contract Vulnerability Detection](https://mlsanity.com/paper/2410.09381/) (2024)
- [solc-verify: A Modular Verifier for Solidity Smart Contracts](https://mlsanity.com/paper/1907.04262/) (2019)
- [Logic Meets Magic: LLMs Cracking Smart Contract Vulnerabilities](https://mlsanity.com/paper/2501.07058/) (2025)
- [Identifying Vulnerabilities in Smart Contracts using Interval Analysis](https://mlsanity.com/paper/2309.13805/) (2023)
- [Leveraging Slither and Interval Analysis to build a Static Analysis Tool](https://mlsanity.com/paper/2410.23766/) (2024)

## Abstract (arXiv)

The high rate of false alarms from static analysis tools and Large Language Models (LLMs) complicates vulnerability detection in Solidity Smart Contracts, demanding methods that can formally or empirically prove the presence of defects. This paper introduces a novel detection pipeline that integrates custom Slither-based detectors, LLMs, Kontrol, and Forge. Our approach is designed to reliably detect defects and generate proofs. We currently perform experiments with promising results for seven types of critical defects. We demonstrate the pipeline's efficacy by presenting our findings for three vulnerabilities -- Reentrancy, Complex Fallback, and Faulty Access Control Policies -- that are challenging for current verification solutions, which often generate false alarms or fail to detect them entirely. We highlight the potential of either symbolic or concrete execution in correctly classifying such code faults. By chaining these instruments, our method effectively validates true positives, significantly reducing the manual verification burden. Although we identify potential limitations, such as the inconsistency and the cost of LLMs, our findings establish a robust framework for combining heuristic analysis with formal verification to achieve more reliable and automated smart contract auditing.