# Manticore: A User-Friendly Symbolic Execution Framework for Binaries and Smart Contracts

## TL;DR

Manticore is an open-source, flexible symbolic execution framework designed for analyzing binaries and smart contracts, enabling users to find bugs and verify code correctness across diverse environments.

## Contribution

It introduces a customizable, architecture-agnostic symbolic execution tool supporting both traditional binaries and Ethereum smart contracts.

## Key findings

- Successfully identified bugs in client code
- Verified correctness of smart contracts
- Supported diverse execution environments

## Abstract

An effective way to maximize code coverage in software tests is through dynamic symbolic execution$-$a technique that uses constraint solving to systematically explore a program's state space. We introduce an open-source dynamic symbolic execution framework called Manticore for analyzing binaries and Ethereum smart contracts. Manticore's flexible architecture allows it to support both traditional and exotic execution environments, and its API allows users to customize their analysis. Here, we discuss Manticore's architecture and demonstrate the capabilities we have used to find bugs and verify the correctness of code for our commercial clients.