---
name: "mythril-evm-symbolic-execution"
description: "Detect smart contract vulnerabilities using symbolic execution and SMT solvers with Mythril."
metadata:
  author: "ConsenSys"
  version: "1.0.0"
  runtime_compatibility:
    - "codex"
    - "claude-code"
    - "cursor"
    - "windsurf"
triggers:
  - "run mythril security analysis"
  - "symbolic execution smart contract"
  - "detect unprotected selfdestruct"
permissions:
  fs_read: true
  fs_write: "workspace"
  shell_exec: false
  net_access: false
---

# Mythril EVM Bytecode Security Analysis

Analyzes Ethereum smart contract bytecode with Mythril: symbolic path exploration, SMT constraint solving (Z3), detecting integer overflows, suicidal contracts, and unprotected selfdestruct operations.

## When to Invoke
Invoke this skill whenever you need to:
- run mythril security analysis
- symbolic execution smart contract
- detect unprotected selfdestruct

## Execution SOP & Rules
1. Execute myth analyze contracts/MyContract.sol --execution-timeout 300 to analyze source files.
2. Tune symbolic search depth with --max-depth to balance audit completeness vs analysis runtime.
3. Review generated transaction sequences illustrating step-by-step exploit paths.
4. Combine Mythril symbolic execution with Slither static analysis for comprehensive contract audits.

## 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.