This project evaluates ESBMC, a formal verification tool, for its ability to detect common vulnerabilities in Ethereum smart contracts. A benchmark suite of Solidity contracts was developed, each containing one or more known issues based on the Smart Contract Weakness Classification (SWC) Registry. These contracts were tested using ESBMC, and the outcomes were analyzed to assess the tool’s effectiveness, limitations, and potential improvements.

- Create a suite of deliberately vulnerable smart contracts

- Evaluate ESBMC’s ability to detect each vulnerability

- Highlight areas where ESBMC performs well or fails

- Provide recommendations for improving ESBMC and similar tools

- Solidity: for writing smart contracts

- ESBMC: for bounded model checking and formal verification

- SWC Registry: for vulnerability definitions and structure

The benchmark includes examples of 33 different SWC vulnerabilities such as:

- Reentrancy (SWC-107)

- Integer Overflows/Underflows (SWC-101)

- Unchecked Call Return Values (SWC-104)

- Deprecated Functions (SWC-111)

- Improper Signature Verification (SWC-122)

- And many others

Out of 33 vulnerabilities:

- ✅ 5 Fully Resolved

- ⚠️ 6 Resolved by recent Solidity versions (not ESBMC)

- 🔧 8 Feasible to resolve with ESBMC enhancements

- ❌ 10 Not feasible due to tool or language limitations

- ❓ 4 Not analyzed in the scope of this study

ESBMC has proven useful for detecting several common vulnerabilities, but its Solidity integration is still in early stages. Key improvements include support for full contract analysis, handling object-oriented features, and expanding pattern-based checks. The benchmark created in this project can be reused and extended to help strengthen future verification tools.

Special thanks to Dr. Lucas C. Cordeiro and the Systems and Software Verification Group at the University of Manchester for their support and guidance.