​
What is the state space?

The state space represents a set of possible ways that a software program can behave. Each “state” is defined by the inputs and environmental conditions that cause a specific outcome or behavior, while the space is the sum of all possible states.

The state space for smart contracts is the set of reachable execution states that a set of interoperating smart contracts can reach. Each state is driven by the possible input values and conditions that execute code paths throughout the set of contracts. The state space and possible paths can be extremely large and in some cases inifnite (known as state space explosion).

​
Complete EVM Semantics

A full EVM semantics model provides a mathematically precise description of every EVM opcode and its effect on the blockchain state. By coupling symbolic execution with this formal model no aspect of execution is overlooked. This means the symbolic execution engine will theoretically be able to produce and capture every behavior and low level details (e.g. account balance updates, reverts, events, etc) with verifiable accuracy and completeness. This leads to high-fidelity coverage of possible execution paths, edge cases, and behaviors.

​
Symbolic execution

Symbolic execution is a program analysis technique that uses symbols rather than concrete values for inputs, allowing it to explore multiple execution paths simultaneously. As the program executes, it builds path constraints—mathematical conditions that must be true to follow each path. Constraint solvers then determine which input values satisfy these conditions, effectively converting program logic into systems of equations. This approach reveals potential behaviors across the program’s entire state space, making it powerful for finding bugs, vulnerabilities, and verifying correctness.

​
Structured dynamic inputs

Generating structured dynamic inputs means that the symbolic execution engine automatically discovers and produces the specific concrete input values that satisfy the code’s logical constraints in a systematic way (e.g. parameters types, addresses, etc ). This leads to far more comprehensive testing while minimizing guesswork or manual enumeration.

  1. Structured: The inputs are not random (as compared to fuzzing). They adhere to the program’s (or contract’s) structure and constraints—things like allowed ranges of integers, valid array lengths, or permitted function-call patterns. The tool enforces these constraints as it explores the code, ensuring each generated input makes sense within the rules of the EVM and smart contract.
  2. Dynamic: These inputs are determined during exploration as the symbolic execution explores different execution paths, and solved mathematically. This maximizes coverage, depth, path exploration and edge case discovery, as opposed to randomly generated inputs.

​
Test case

A test case involves executing a sequence of transactions of a smart contract program on a set of concrete inputs and state conditions, and checking the resulting output and state behavior.

​
Automatic test case/suite generation

The automated process of producing structured and dynamic input values and the resulting contract states and environment conditions for each explored execution path throughout the program. This represents the actual behavior of the program which includes both expected (correct) behaviors, and bugs (if any exist!). The test cases can be used to validate the correctness, security, and functional behavior of the smart contract.