为什么选择模糊测试而不是形式化验证？

Trail of Bits 解释为何多数审计选择模糊测试而非形式化验证：复杂代码库上“证明无缺陷”往往不可行（常需重写代码或依赖自定义摘要），而模糊测试能以更低的技能与时间成本发现同类问题；文章以 DAI、Compound V3 等不变式为例展开讨论。