帖子
sopleat（E卫兵）
形式验证证明的是模型内正确
形式验证把合约应满足的性质写成数学规格，再证明实现不会违反这些性质。它可以覆盖普通测试难以穷举的大量输入，特别适合余额守恒、权限边界和状态转换等关键规则。相比“跑了很多测试都没出错”，数学证明提供了更强的功能正确性保证。
但证明永远相对于规格成立。若团队把错误需求写进规格，工具会严谨证明一套错误规则；若模型省略预言机、管理员或跨合约依赖，真实系统仍可能失败。编译器、部署配置和升级过程也可能不在证明范围内。$ETH合约不可轻易撤回，强证明重要，边界说明同样重要。
评估形式验证项目，要问证明了哪些不变量、对应哪个代码版本、哪些外部组件被假设可信。它应与审计、模糊测试和运行监控配合，而不是取代所有安全工作。最可靠的报告会同时列出已证明性质和未覆盖部分，让用户知道结论在哪里有效。
