A Smart contract is a self-executing code (agreement)between two or more parties deployed and executed in a distributed ledger platform.
### Formal Verification
Static analysis and a maths-based technique are called formal methods to check the system design and its properties. And it contributes to the safety and steadiness of the system as well as the functional correctness of the smart contract.
### Symbolic execution
All paths exploration.The execution makes use of “symbols” as inputs to the program and the results are expressed in terms of the symbolic inputs.
### Bytecode
Bytecode is written in low-level language that executes in environment like Ethereum Virtual Machine (EVM)).
### Model Checking
Model checking is a method for automatically verifying a system model with finite states against its specification. When it is used in smart contracts, model checkers perform verification of contract-level models, mainly transition systems, against a temporal logic specification.
### Runtime Verification and Testing
Runtime verification is a lightweight verification technique that checks the properties of a running program. In the domain of smart contracts, the term trace often denotes a sequence of instructions executed by a blockchain platform, while it can also refer to a sequence of function invocations or events emitted by a smart contract. Runtime verification usually provides a reactive defense against vulnerabilities or violations of correctness at runtime and can potentially identify vulnerable states that could not be reached by model checking or symbolic execution, due to the state or path explosion.
### Theorem Proving
Verification based on theorem proving involves encoding a system and its desired properties into a particular mathematical logic.
### Fuzzing
Fuzzing is a technique for finding software bugs by inputting a large number of randomized test cases to a program. The goal is to discover unexpected or undefined behavior, such as crashes or memory leaks, that may indicate a vulnerability. Fuzzing can be automated using specialized tools, and is often used in security testing and software development. It can be used to test a wide range of software, including operating systems, file formats, and network protocols.
