Security analysis tools and mechanism

There are several techniques to check the correctness of programs. First, we have unit testing, which is a common method. Second, we have property-based testing, i.e., fuzzing. At the next level, we have model checking, and finally, formal proofs are the most advanced technique to ensure the correctness of programs, in this case, smart contracts. Testing includes unit tests, integration tests, full end-to-end tests, and property-based testing, also called fuzzers.

Static analysis allows us to check the code against a set of coding rules to find code defects. The code does not execute; instead, it is statically checked. On the other hand, there is a dynamic analysis technique where the code is executed to find bugs and is tested against test criteria. Dynamic analysis usually constitutes unit tests and is not considered a formal verification technique. Static analysis using formal techniques is used to formally verify the correctness of the...