## 4 Smart Contract Vulnerability Detection Tools
### Model Detection Method  
Model detection is a method for finding weaknesses in smart contracts that is based on formal specification descriptions and automated verification. By creating a model and iterating through its state space, the model detection approach finds all potential states and the transfer linkages between them. It can then check the characteristics of these states to see if any vulnerabilities are present. The model detection method's primary steps for finding smart contract vulnerabilities are as follows:  
The smart contract can be formally tested by utilizing a model detection tool after being converted into a finite state machine model. A finite state machine or a Kripke structure, an extension of a finite state machine, can be used to describe the behavior of concurrent and distributed systems, which is typically used to build the model. A finite state machine is a mathematical model that describes finite states and transfers between states. Establishing the characteristics  
The properties that need to be validated must be identified after the model has been constructed. To represent the correctness and security of a smart contract, attributes are frequently utilized. They include security, correctness, and reachability. For illustration, security characteristics could include preventing double payments, preventing overflow protection, denial-of-service attack protection, etc. Validate the attributes using model testing tools  
The model detection tool is used to validate the constructed model and attribute. The model detection tool will automatically cycle through all the conceivable states, transfer relationships between states, and determine whether any states or paths match the requirements. A vulnerability exists and needs further investigation and correction if a state or path that satisfies the attribute is discovered. SaferSC [34] is a smart contract vulnerability detection model that utilizes deep learning techniques to achieve better accuracy in detecting three different types of contract vulnerabilities. This model is based on Maian and goes beyond it by analyzing the operation code level of smart contracts in detail. The SaferSC model constructs a sequential model of the operation code of Ethereum using LSTM network (Long Short Term Memory). This allows the model to perform accurate and intelligent detection of security vulnerabilities of smart contracts. LSTM network is a type of recurrent neural network (RNN) that is particularly effective at processing sequential data, such as natural language or time series data. By using deep learning techniques, SaferSC is able to improve the accuracy of smart contract vulnerability detection compared to traditional methods. This can help prevent security breaches and protect users' assets in the blockchain ecosystem. DR-GCN is a contract graph-based approach for discovering vulnerabilities in smart contracts. This method transforms the source code of a smart contract into a highly semantically expressed contract graph and then constructs a security vulnerability detection model using a graph convolutional neural network. The model is capable of detecting vulnerabilities such as reentrancy, timestamp dependency, and dead loops in two platforms, Ether and Vitelink. Although there are many automatic smart contract vulnerability verification tools available, most of them have certain shortcomings. First, their testing methods are simple and can only cover a limited range of vulnerabilities. Second, the code coverage is often low, resulting in a high rate of missing and false positives in the test results. Third, it is difficult to achieve fully automated detection and clear detection. Fourth, the usual detection time is long, and the mining speed of vulnerabilities is slow, leaving room for improvement in terms of expanding vulnerability coverage and improving detection efficiency.