About Project

Symbolic execution tool on Smart Contracts and Binaries


  • Input Generation: Manticore automatically generates inputs that trigger unique code paths
  • Error Discovery: Manticore discovers bugs and produces inputs required to trigger them
  • Execution Tracing: Manticore records an instruction-level trace of execution for each generated input
  • Programmatic Interface: Manticore exposes programmatic access to its analysis engine via a Python API

Manticore can analyze the following types of programs:

  • Ethereum smart contracts (EVM bytecode)
  • Linux ELF binaries (x86, x86_64 and ARMv7)