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