---
name: "manticore-symbolic-binary-executor"
description: "Analyze binaries and EVM smart contracts with symbolic execution and constraint solvers."
metadata:
  author: "Trail of Bits"
  version: "1.0.0"
  runtime_compatibility:
    - "codex"
    - "claude-code"
    - "cursor"
    - "windsurf"
triggers:
  - "run manticore analysis"
  - "symbolic execution binary manticore"
  - "generate inputs manticore"
permissions:
  fs_read: true
  fs_write: "workspace"
  shell_exec: false
  net_access: false
---

# Manticore Symbolic Execution for Binaries & Contracts

Applies dynamic symbolic execution using Trail of Bits Manticore: symbolic input generation, path exploration, detecting reachable assertion failures, and analyzing Linux ELF binaries.

## When to Invoke
Invoke this skill whenever you need to:
- run manticore analysis
- symbolic execution binary manticore
- generate inputs manticore

## Execution SOP & Rules
1. Initialize Manticore instance with m = Manticore(binary_path).
2. Define symbolic buffers using m.make_symbolic_buffer(size).
3. Register hooks on target memory addresses to inspect solver constraints.
4. Extract concrete input byte sequences from satisfiable execution paths.

## Verification Checklist
- Run local linting, syntax validation, and type-checks before reporting completion.
- Ensure all created or modified files adhere to workspace boundaries and avoid uncommitted secrets.
- Verify tests or build commands exit cleanly with return code 0.