State Space is a visual formal verification solution for Ethereum-compatible (EVM) smart contracts, providing formally derived test case generation, advanced security analysis, and code behavior validation.

What is State Space?

State Space helps you understand, validate, test, and document the behavior of smart contracts with mathemtical precision. leverages dynamic symbolic execution and a fully defined EVM semantics model to automatically generate and visualize the complete state space of multi-contract protocols. Rather than proving absence of bugs, it systematically:

  • Discovers all feasible execution paths by solving path constraints with SMT solvers
  • Generates concrete input values that trigger each unique execution path
  • Visually maps the entire behavior space of your smart contracts
  • Surfaces both expected behaviors and edge cases that traditional testing often misses
  • Uses fully defined EVM semantics for deep path coverage and edge case discovery simulating on-chain execution

Unlike manual testing where engineers create specific test cases, State Space automatically explores your contract’s behavior space, creating a comprehensive visual representation that allows security engineers to inspect actual contract behavior under all possible inputs and conditions.

What can I do with it?

The state space can be used to:

  • Validate business logic and compliance requirements
  • Perform advanced security analysis
  • Auto-generate code behavior and testing documentation for regulatory compliance
  • Generate high coverage test suites, or fill missing test scenarios for existing test suites
  • Uncover unknown unknowns
  • Cover deep edge cases
  • Simulate complex scenarios
  • Surface technical risk
  • Standardize testing across teams (instead of manual)
  • Automate regression test case generation and diffs
  • Export fully reproducible test suites to Foundry and Hardhat

Getting Started


Learn more about State Space


Additional Resources