形式验证究竟证明什么
区块链形式验证的应用边界是什么，首先要区分“符合规格”与“没有任何风险”。本文聚焦智能合约，不将结论扩展为对整个区块链系统的安全证明。
以太坊开发者文档将形式验证解释为：用数学模型和形式化规格描述要求，再检查实现是否满足这些要求。规格可以涉及访问权限、余额约束等安全性质，也可以涉及系统能否最终推进的活性性质。证明始终针对所描述的性质，而不是所有可能的需求。
规格与模型决定覆盖范围
适合验证的要求，应能明确表达输入条件、状态变化和预期结果。例如，“未获授权的账户不能修改某项配置”比“合约足够安全”更容易形成可检验的命题。若规格遗漏了一类权限操作，即使其他性质得到证明，也不能据此认为遗漏部分已经安全。
模型的抽象层次同样重要。只描述业务状态变化，不等于覆盖每个底层执行细节；检查单个函数，也不自动覆盖多个合约的交互。判断结论时，应同时看验证了什么，以及哪些行为未被纳入模型。
外部条件不是自动成立的保证
如果证明以外部调用满足某种约束为前提，实际调用对象也必须满足该约束，结论才适用。不能把“假设依赖行为正确”理解成“已经证明依赖正确”。
“操作最终完成”还应与“执行终止”区分。交易因资源耗尽而终止，并不代表业务成功；证明状态不会出现某种错误，也不直接证明用户请求最终一定得到处理。
部署与升级会改变证明对象
OpenZeppelin的可升级合约文档强调，代理状态需要通过初始化逻辑正确设置，并防止不应发生的重复初始化；升级还必须保持存储布局兼容。这说明实现代码之外，初始化和状态解释方式也影响实际行为。
如果验证只覆盖初始化后的正常操作，就不能据此排除初始化阶段的问题。旧版本的证明也不能直接作为新版本的证明：代码、状态布局或初始化路径变化后，需要重新检查相关性质及其假设是否仍然成立。
常见问题：通过验证是否就够了
形式验证不能替代全部测试和安全审查。它适合检查边界明确、可以形式化表达的关键性质；测试和审查则能从实际交互、部署配置及需求遗漏等角度提供补充。
阅读验证结论时，至少应确认对应的代码版本、性质清单、前置条件、外部依赖假设和排除项。“已通过形式验证”只有与这些范围说明一起出现，才足以表达其保障力度。