符号执行（Symbolic Execution）是一种程序分析技术：不拿具体输入把程序跑一遍，而是把输入当成未知数，把每条执行路径变成数学方程，再交给约束求解器（Constraint Solver）求解。
举个例子。函数 f(x) 在 x > 0 且 x*x == 4 时计算 1/(x-2)。具体测试要试 x=1、x=2……；符号执行把 x 记作 α，遇到 if 就收集约束：走外层要求 α > 0，走内层还要求 α² = 4。求解器解出 α = 2，于是它知道“输入 2 会走到除零那一步”。程序不必真的跑，也能生成能触发错误的输入。
打个比方：查迷宫有没有出口，具体测试是派机器人乱跑；符号执行把每个岔路写成“若在 A 且选左，则到 B”的条件，再用代数解出哪条路能到出口。它把“跑程序”换成了“解方程”。
和相邻概念的区别：
| 技术 | 是否真执行 | 输入形式 | 典型产出 |
|---|---|---|---|
| 具体测试 | 是 | 具体值 | 通过/失败 |
| 模糊测试（Fuzzing） | 是 | 变异生成的值 | 崩溃样本 |
| 符号执行 | 通常不实际执行 | 符号表达式 | 可达路径、触发输入 |
| 抽象解释（Abstract Interpretation） | 否 | 抽象值 | 近似不变量 |
符号执行比随机测试更有的放矢，因为它能反推出满足条件的具体输入。但它有硬伤：分支一多，路径数量指数增长，即路径爆炸（path explosion）；循环、指针、并发、系统调用都难建模；约束求解也可能解不出来。于是有了混合执行（Concolic Execution）：先用具体输入跑一遍，沿途收集约束，再对某个分支取反去求解，引导探索新路径。
这与 AI 自动找漏洞、自动验证关系很近。自动找漏洞可以看成“让机器生成能触发断言的输入”：符号执行提供精确的路径约束，机器学习常用来做路径调度，预测哪些分支更可能出错，优先探索、及时剪枝；约束求解器也会吸收学习型启发式来加速。自动验证则走另一面：若某条路径解出违反断言的输入，这就是反例；若在限定深度内穷尽路径都解不出反例，就近似证明断言成立。有界模型检验（Bounded Model Checking）就是“展开程序、化成公式、求解验证”的典型思路。
对从业者来说有两个实际意义：写代码时，边界、断言、纯函数逻辑越清晰，越容易被这种分析精确处理；看安全工具报告时，要问一句“这条路径真的可行吗”，不可行路径会带来误报。对普通人来说，很多自动化安全检测、编译器告警、智能合约审计背后，都有“把程序当方程解”的影子。它不是万能钥匙，但把“机器自己找漏洞”从碰运气推进了一步。具体工具差异大，以官方文档为准。