测试告诉你「没找到错」，证明告诉你「按这条规范不可能错」——这两句话的差别，就是形式验证和常规测试的全部差别。在 DeFi 协议的审计报告里，你越来越常看到「已做形式验证」这样的句子，但它既不是保险单，也不是万能章。搞清楚这台工具能证什么、不能证什么，你才知道一份「证明过的协议」到底给了你多厚的安全垫。
先说它和测试的区别。常规测试是抽样：工程师写出几千个用例，覆盖他想到的场景，没跑挂不代表没有别的跑挂方式。形式验证换了个思路：把合约里你认为永远不该被破坏的规则写成数学命题（术语叫不变量或性质），再用自动化工具穷尽所有可能的执行路径去证明这条命题恒成立。常见的用法有三类：一类是定理证明器，把代码和规范都翻译成逻辑语言，人工引导证明过程；一类是符号执行工具，让变量取「符号值」而不是具体数字，自动探索所有分支，找出任何能让断言失败的路径；还有一类是模型检测，在小规模状态空间里把所有状态走一遍。对借贷、AMM、金库这类「账本类合约」，最常被验证的性质也最朴素：金库里的份额总数和底层资产不能被凭空多造出来，抵押率低于阈值的账户不能被提款，权限函数不能被客户合约调用。
但证明只覆盖「写进规范的部分」，这是第一个大边界。规范本身是人写的：你证明的是「余额守恒」，那攻击者如果走的根本不是改余额的路径呢？历史上不少事故恰恰出在规范之外的缝隙里——预言机喂进来的价格异常、代币实现不符合 ERC-20 的直觉（比如转账会额外扣费的转账税代币）、外部依赖返回了规范假设不会出现的值。形式验证工具通常假设外部调用都守规矩，而现实链上环境里没有这个假设。所以一份验证报告必须连同它的规范一起读：证了哪几条性质、用了什么假设、哪些模块被建模简化过、哪些函数被标记为「超出范围」。只有「通过了某某工具」四个字而没有规范细节的宣称，信息量约等于零。
第二个边界是分层覆盖：EVM 字节码、编译器、合约源码，每层都可以验证，但每层的证明只在自己的抽象层成立。从源码到字节码中间隔着编译器，编译器本身的缺陷不在源码层证明的覆盖范围内；字节码层验证只针对执行语义，管不到业务逻辑选错了公式。这也是为什么严肃项目通常把三层都跑一遍再拼起来看。
第三条边界是「代码对，不等于系统对」。DeFi 协议的运行时风险有一大半在代码之外：治理参数被投票改到危险区间、多签密钥被社工、预言机源站被操纵、升级合约被换掉实现。这些都不是智能合约代码的数学性质，形式验证天然不碰它们。它们对应的防线是治理时间锁、权限审查、喂价偏离监控，与验证工具是并列关系，不是替代关系。
对普通用户来说，正确的用法是把「有形式验证」当成一个可核查的加分项，而不是结论。核查路径有三步：先找项目方公开的验证规范文档，看它证明了哪几条性质、是不是你关心的那几条（比如你是不是最在意「清算逻辑不能被绕过」）；再看工具与版本记录，验证是针对哪个提交号做的，之后的改动有没有重跑；最后看审计、验证、监控三件套是否齐备——只做验证不请审计、或只请审计没有链上监控的项目，等于把同一道门只装了一半锁。
还需要警惕一种营销话术：「我们的数学被证明了」听起来像「我们的资金绝对安全」，其实两者之间隔着上面所有边界。证明的命题越接近业务核心（例如某个利率模型在任何输入序列下都不会出现负利率），价值越大；证的是越边缘的性质（例如某个事件一定被触发），价值越像装饰。同一句「已通过形式验证」，背后可能是核心清算逻辑的全覆盖，也可能只是工具顺手跑出来的边角料。
最后给一份自查清单。看到一份带形式验证的审计报告，依次问五件事：证明的是哪个版本哪个提交；规范文本在哪里，覆盖了哪几条业务不变量；建模时对外部调用、代币行为、预言机输入做了什么假设；哪些模块明确不在范围内；验证之后代码又改了多少。五个问题都有答案的，这句宣称才值得进你的信任清单。协议实现会持续演进，工具链也在更新，具体项目的验证范围请以其官方仓库和报告为准，核查时留意发布日期。本文只做机制说明，不构成投资建议。
发表评论
还没有评论，来说两句吧。
评论区为展示样式，提交不会被处理。