Mythril 是由 Consensys Diligence 维护的 EVM 字节码符号执行安全分析工具，用于检测 Solidity 智能合约漏洞。与 Slither、Semgrep 等基于代码模式匹配的静态分析器不同，Mythril 通过构造有效交易序列来证明漏洞是否真正可被利用，因此速度更慢但对某些漏洞类型更精确。它使用 LASER 符号虚拟机跨多笔交易探索所有可达合约状态，再将路径约束交给 Z3 SMT 求解器生成具体利用输入。
主要能力：将 Solidity 编译为字节码后符号执行，分析对象是字节码而非源码；检测模块映射到 SWC 编号，包括 ether_thief(SWC-105)、suicide(SWC-106)、delegatecall(SWC-112)、reentrancy(SWC-107)、integer(SWC-101)、unchecked_retval(SWC-104)、tx_origin(SWC-115)、exceptions(SWC-110)、arbitrary_write(SWC-124)、multiple_sends(SWC-113) 等。可运行指定模块（-m）或排除模块（--exclude-modules）。支持文本、JSON、markdown、jsonv2 输出，可分析本地文件、已部署合约（--address 配合 --rpc-url）以及原始字节码（--bin-runtime）。
使用方式：推荐 Docker 安装，docker pull mythril/myth，docker run -v $(pwd):/src mythril/myth analyze /src/Contract.sol；也可 pip3 install mythril（需 Python 3.8-3.12 与 C++ 编译器，Z3 构建失败时可先装 libz3-dev 或 brew install z3）。命令为 myth analyze，旧式 myth -x 已弃用。分析深度由 -t 控制交易笔数，默认 2；-t 3 可发现跨函数重入、闪电贷等多步漏洞，但耗时可能增加 10 至 100 倍。因默认无超时，生产使用需设置 --execution-timeout 与 --solver-timeout，还可用 --max-depth、--loop-bound、--call-depth-limit、--strategy 等参数。需用 --solv 指定与 pragma 匹配的 solc 版本，导入问题可用 --solc-args 添加 --base-path 与 --include-path。
适用场景：上线前深度安全扫描、CI 流水线集成、对已部署合约做链上分析。限制：速度慢且耗时随交易数指数增长；只理解字节码，输出引用字节码偏移而非源码行；不替代静态分析，可能产生误报（如自定义 assert 触发 SWC-110）；超时无结果不代表合约安全；对可升级合约支持有限；链上分析因需 RPC 解析存储与外部依赖而更慢。建议先用 Slither 快速筛查、再用 Mythril 深入分析并人工复核交易序列。