从 “代码即法律” 到 “规范即法律”：形式化验证如何终结 DeFi 34 亿美元的漏洞危机
一个舍入错误 —— Solidity 整数除法中不足一分钱的精度损失 —— 在不到 30 分钟的时间内，从九个区块链上的 Balancer 中抽走了 1.28 亿美元。这些池子已经运行了数年。代码经过了多次审计。没有人发现它。这就是 2026 年 DeFi 安全的状态：数百亿美元被保护在一个已被证明一再失败的范式之下。
现在 a16z crypto 正在提出一种彻底的反思。在其 2026 年的“大创意”报告中，这家风险投资公司认为，行业必须放弃“代码即法律”（code is law）—— 即已部署的智能合约代码是最终权威的这一基本信念 —— 并将其替换为“规范即法律”（spec is law），即数学定义的安全属性成为可执行的标准。这一转变可能会从根本上重塑协议的构建、审计和防御方式。
审计无法解决的 34 亿美元难题
数据说明了一个令人沮丧的事实。仅在 2025 年，加密货币行业因盗窃损失了超过 34 亿美元，其中 Bybit 的遭黑事件占了 15 亿美元。在 2025 年上半年，智能合约漏洞造成了约 2.63 亿美元的损失。累计来看，顶级的 DeFi 漏洞已从协议中榨取了超过 107.7 亿美元。
传统的安全模型 —— 编写代码、聘请审计、部署并祈祷 —— 已经触及了天花板。即使是拥有顶级公司多次审计的资金雄厚的协议仍然容易受到攻击。Balancer 的漏洞毫无疑问地证明了这一点：一个隐藏在眼皮底下多年的漏洞，被专业的安全审查所忽略，一旦被发现，在几分钟内就被利用了。
更令人不安的是攻击手段的日益复杂。2024 年闪电贷漏洞激增，占符合条件的利用漏洞的 83.3%。2025 年大多数大型黑客攻击同时结合了二至四种漏洞类型。仅朝鲜黑客在 2025 年就窃取了 20.2 亿美元，同比增长 51%。攻击者的智能化速度比防御者更快。
剖析 1.28 亿美元舍入错误
Balancer 的漏洞值得仔细研究，因为它完美地说明了为什么“代码即法律”会失效。2025 年 11 月 3 日，一名攻击者利用了 Balancer 的 ComposableStablePools 处理小额交换时的一个数学漏洞。
事情是这样的：当代币余额被推到特定范围（8-9 wei）时，Solidity 的整数除法会导致严重的精度损失。_upscaleArray 函数在缩放过程中向下舍入，导致池子的不变性（invariant）—— 即应该管理公 平汇率的数学常数 —— 被低估。这人为地压低了 BPT（Balancer 池代币）的价格。
攻击者利用这一点，在包含 65 个以上操作的单个 batchSwap 交易中执行了三阶段交换序列：
- 价格压制：将大量 BPT 兑换为基础代币，将一个代币的余额推向 8-9 wei 的临界阈值，使舍入错误最大化。
- 廉价收购：以人为压低的价格铸造或购买 BPT。
- 全额赎回：立即按全额价值将 BPT 赎回为基础资产。
整个攻击是在一个已部署智能合约的构造函数中执行的 —— 这是一个单一交易，抽干了 Ethereum、Base、Arbitrum、Avalanche、Optimism、Gnosis、Polygon、Berachain 和 Sonic 上的 1.2864 亿美元。社区的快速响应挽回了约 1900 万美元，但绝大部分资金已损失。
关键教训：这并非一个奇特的漏洞。这是一个数学不变性的违规 —— 这种漏洞根据定义，形式化规范（formal specification）是可以捕捉到的。
“规范即法律”究竟意味着什么
a16z 的提议在两个层面上运作：静态（部署前）和动态（部署后）。
在静态方面，DeFi 安全必须从验证精心挑选的局部属性转向系统地证明全局不变性。问题不再是“这个函数是否正确处理了边缘情况？”，而是“整个系统在所有可能的输入和状态下，是否保持其核心数学属性？”
这就是 Certora Prover 和 Runtime Verification 的 K Framework 等形式化验证工具发挥作用的地方。这些工 具将智能合约字节码与定义预期行为的数学规则进行比较，检查每个可能的合约状态和执行路径。例如，Certora Prover 使用以 CVL（Certora 验证语言）编写的规范，通过静态分析和约束求解来检测属性违规。
在动态方面，这些相同的不变性变成了实时护栏 —— 每笔交易都必须满足的运行时断言。如果一笔交易会违反核心安全属性，它会自动回滚。这就是“最后一道防线”的概念：即使是新颖的、以前从未见过的攻击，也必须满足系统的基本安全属性。
这种方法的优雅之处在于其不对称性。攻击者必须寻找违规行为；防御者只需要定义“正确”的样子。正如 a16z 所说：“即使是新颖的攻击也必须满足保持系统完整的相同安全属性，因此剩下的唯一攻击就是微小的或极其难以执行的。”
谁已经在以此方式构建
“规范即法律”（spec is law）的愿景并非纯粹的理论。几个主要的协议已经开始将形式化验证作为其开发过程的核心部分。
Aave 是按 TVL 计算最大的借贷协议，它已将 Certora Prover 直接集成到其持续集成（CI）流水线中。代码的每一次更改都会在合并前根据形式化规范进行自动验证。这不只是偶尔的审计，而是对每一次提交进行的数学证明。
Uniswap V2 使用 Runtime Verification 的 K 框架对其核心的 “x*y=k” 做市商模型进行了形式化验证。验证涵盖了数学模型的形式化、其智能合约的实现，以及对四个关键功能的编译字节码进行的符号执行。
Kamino 是一家基于 Solana 的借贷协议，于 2025 年初开始使用 Certora Prover 检查关键的不变量。XRP Ledger 也已在协议层面实现了不变量检查。这些并非以太坊特有的进展 —— “规范即法律” 的方法正在跨区块链生态系统传播。
AI 与形式化验证的结合：Certora 的 Composer
形式化验证最显著的障碍之一是其复杂性。编写形式化规范需要大多数开发团队所缺乏的专业知识。这种情况正在改变。
2025 年 12 月，Certora 推出了 AI Composer —— 一个开源的 AI 编程平台，它将形式化验证直接嵌入到代码生成过程中。与优先考虑速度的通用 AI 编码工具不同，AI Composer 确保每个 AI 生成的代码片段在执行前都符合数学安全规则。
该平台代表了形式化验证潜在的民主化。如果 AI 可以协助编写规范、提出不变量并降低手动证明工程的成本，那么除了目前少数能够负担得起专门形式化验证工程师的团队外，“规范即法律” 将变得触手可及。
这种 AI 与验证的融合也呼应了 a16z 的观察，即当前的 DeFi 安全应该 “系统地证明全局不变量，而不是验证手动挑选的局部不变量”。AI 可以比人类工程师更广泛地探索规范空间，潜在地捕捉到像 Balancer 的舍入误差那样逃过人工审查的微妙数学违规行为。
法律与治理影响
“规范即法律” 带来的影响超出了代码本身。如果一个协议发布了定义其预期行为的形式化规范，这些规范可能会成为评判该协议的法律标准。
在 “代码即法律”（code is law）的体系下，对已部署代码的任何利用在技术上都是 “按预期运行” 的 —— 代码完全按照其编程方式执行，即使那不是开发者的本意。而在 “规范即法律” 下，形式化规范定义了意图。协议开发者将对偏离已发布规范的行为负责，但不对这些规范之外的每个可能利用向量负责。
这建立了一个更清晰的问责框架。如果 Balancer 发布了一个形式化规范，声明无论交易顺序如何，池的不变量必须保持在定义的范围内，那么舍入误差利用将是一个明显的规范违规 —— 并且可能成为法律追索或保险索赔的依据。
挑战与局限性
“规范即法律” 的论点引人入胜，但也面临着现实障碍。
规范的完整性 是根本挑战。你如何形式化地规定每一个重要的属性？规范是由人编写的，人可能会遗漏关键属性 —— 正如审计员会遗漏关键漏洞一样。一个未能捕捉到正确不变量的规范会提供虚假的安全感。
可组合性风险 增加了另一层难度。DeFi 的价值来自于协议之间的相互协作。形式化验证单个协议的不变量并不能保证当该协议以意外方式与其他协议组合时的安全性。协议之间的交互面仍然是一个在很大程度上尚未规范化的前沿领域。
性能和成本 是现实考量。形式化验证的计算成本很高。运 行时不变量检查会增加每笔交易的 Gas 成本。对于每秒处理数千笔交易的高频协议来说，这些成本至关重要。
采用惯性 可能是最大的障碍。大多数 DeFi 团队在激烈的竞争压力下发布代码。在开发流水线中增加形式化验证会减慢部署速度。除非市场以更高的 TVL 或更低的保险费奖励经过验证的协议，否则采用的动力仍然很弱。
前进之路
尽管存在这些挑战，但发展轨迹是明确的。漏洞利用的代价 —— 2025 年为 34 亿美元，累计达 107.7 亿美元 —— 使得现状难以为继。保险市场、机构资本和监管框架将越来越多地要求可证明的安全保证。
AI 辅助规范编写、成熟的形式化验证工具以及运行时执行基础设施的融合正在降低采用门槛。当 Aave 可以在每次提交时运行 Certora Prover，而 Kamino 可以在 Solana 上检查不变量时，工具链已经从学术研究跨越到了生产基础设施。
行业从 “代码即法律” 向 “规范即法律” 的演进，反映了在每个成熟工程学科中都能看到的模式：从 “我们构建了它且它似乎运行良好” 到 “我们可以从数学上证明它符合其规范”。航空、核工程和半导体设计都经历了这一转变。DeFi 拥有超过 1000 亿美元的 TVL，且依赖于数学的正确性，这一转变早已迟到。
问题不在于 “规范即法律” 是否会成为标准，而在于在它成为标准之前还会损失多少个十亿美元。
BlockEden.xyz 提供企业级区块链 API 基础架构，为跨多个链的 DeFi 应用提供动力。随着形式化验证成为行业标准，可靠的节点基础设施构成了验证协议交互的基础。探索我们的 API 市场，在为安全第一时代设计的基础架构上进行构建。