a16z 的 “规则即法律” 愿景：AI 辅助形式化验证与运行时护栏如何重塑 DeFi 安全

2025 年 12 月，Anthropic 的研究人员将一个 AI 代理指向 405 个现实世界中被利用的智能合约。该代理为其中的 207 个（51%）生成了有效的漏洞利用程序，在模拟资金中窃取了 5.5 亿美元。每次成功利用的成本是多少？仅需 1.22 美元。

这一数据点捕捉到了 2026 年去中心化金融面临的生存危机。2025 年因加密货币黑客攻击损失的 34 亿美元并非源于努力不足——大多数受攻击的协议都经过了审计，有些甚至审计了多次。这是范式的失败。现在，a16z Crypto 提出了一个激进的替代方案：放弃“代码即法律”，拥抱“规范即法律”，通过数学证明的安全属性和实时运行时护栏，使大多数漏洞利用在结构上变得不可能。

34 亿美元的警钟

2025 年的数据令人震惊。加密货币盗窃总额达到 34 亿美元，仅朝鲜的 Lazarus Group 就造成了 20.2 亿美元的损失——创下了纪录。Bybit 交易所 15 亿美元的黑客攻击占年度总损失的 44%。仅三起事件就占盗窃总额的 69%。

但也许比头条数据更令人担忧的是 DeFi 领域发生的事情。2025 年 3 月，一个主要 DeFi 协议中的重入漏洞在不到 90 秒的时间内被榨取了 4700 万美元。该合约曾由三家独立的审计公司进行过审计，而三家公司全都漏掉了它。

这种“审计、被盗、重复”的模式已经上演了数十次。传统的审计是由人类审查员执行的特定时间点的快照，无论技术多么精湛，他们都无法详尽验证复杂智能合约中每一个可能的状态转换。他们能捕捉到常见的模式，却会遗漏新颖的组合。随着 AI 使漏洞发现的成本成倍降低，防御者的容错空间正在缩小到零。

从“代码即法律”到“规范即法律”

自以太坊诞生以来，“代码即法律”一直是加密货币的哲学基石。根据定义，无论智能合约执行什么操作，都是正确的。2016 年的 DAO 黑客攻击考验了这一原则。十年后，a16z Crypto 认为现在是时候彻底弃用它了。

在他们的 2026 年预测报告中，a16z 的研究人员提出了所谓的“规范即法律”——这是一个协议正式定义安全属性（规范）并在从部署前验证到运行时执行的每一层强制执行这些属性的框架。核心见解是：即使是全新的、从未见过的攻击也必须满足保持系统完好的相同安全属性。如果这些属性被严格定义和强制执行，唯一能存活的漏洞利用将是“微小的或极难执行的”。

这不是一次理论演练。这是一个具有两个互补层级的具体工程处方。

第一层：静态形式化验证（部署前）

形式化验证使用数学证明来论证智能合约在所有可能的输入和状态转换下都满足特定的属性——而不仅仅是人类测试人员想到要检查的那些。与探索场景子集的模糊测试（fuzzing）或单元测试不同，形式化验证是详尽无遗的。

这种方法要求协议定义全局不变性（global invariants）：必须始终保持真实的属性。对于借贷协议，不变性可能是：“抵押品的总价值必须始终超过未偿贷款的总价值。”对于 DEX（去中心化交易所）：“任何单次交易提取的价值都不能超过资金池所含的价值。”

加密领域领先的形式化验证公司 Certora 在 2025 年展示了这种方法的力量。在与 Solana 上的 Kamino Finance 合作时，Certora 的 Prover 系统地评估了两个偿付能力不变性，并发现了一个精度损失漏洞——这是一个微妙的舍入错误，允许用户赎回比存款更多的抵押品。没有任何人类审计员发现它。

2025 年，Certora 在整个行业内保障了 1965 亿美元的总锁定价值（TVL），并阻止了 720 多个漏洞进入生产环境。按 TVL 排名的前 20 个 DeFi 协议中，有 14 个（约占该类别的 70%）现在与 Certora 合作。Certora Prover 已经开源，其新的 AI Composer 工具利用机器学习来帮助编写规范并提出不变性建议，大大减少了历史上使形式化验证成本极其昂贵的人工工程投入。

第二层：运行时护栏（部署后）

静态验证在部署前捕捉错误。但对于可升级合约、治理变更、预言机故障或发布后出现的新型攻击向量又该怎么办呢？这就是 a16z 愿景变得激进的地方。

该提案：将安全属性编码为每笔交易都必须满足的运行时断言。如果一笔交易会违反不变性——例如，在单个区块中榨取的资金超过协议定义的资金池百分比——则该交易在状态更改提交之前会自动回滚。

可以将其视为智能合约的断路器。传统的证券交易所会在波动超过阈值时停止交易。运行时护栏也做同样的事情，但由代码强制执行，以区块产生的速度运行，无需人工干预。

Guardrail 是一家专门构建此类基础设施的初创公司，它部署了 295 多个可定制的“护栏”（guards），用于检测异常、模拟风险交易并执行运行时检查。该平台保护着超过 13 亿美元的资产，并能实时自动暂停易受攻击的功能或标记恶意钱包。

a16z 的研究人员指出，“在实践中，迄今为止几乎所有的漏洞利用都会在执行期间触发这些检查中的某一项，从而可能阻止黑客攻击。” 4700 万美元的重入攻击？如果在每笔交易前后对资金池余额进行简单的不变性检查，就能发现它。15 亿美元的 Bybit 黑客攻击？对提现速度和目标地址的运行时监控本可以触发自动暂停。

AI 军备竞赛：进攻与防御的博弈

这种范式转变背后的紧迫性是由一个新的现实驱动的：AI 使得攻击成本下降的速度快于防御能力提升的速度。

Anthropic 的 SCONE-bench 研究描绘了一个令人清醒的现状。其 AI 代理针对 2020 年至 2025 年间部署的 405 个真实世界中被攻击过的合约进行测试，成功率达到了 51%。在 2025 年 6 月之后被攻击的合约（这意味着 AI 没有关于这些特定漏洞的训练数据）中，Claude Opus 4.5、Claude Sonnet 4.5 和 GPT-5 仍然共同产生了价值 460 万美元的漏洞利用。

最引人注目的是：当这些代理针对 2,849 个近期部署且无已知漏洞的合约时，它们发现了两个真实的零日漏洞（zero-day exploits）。来自模拟盗取资金的漏洞利用收益大约每 1.3 个月翻一番，而每次成功利用的计算成本在六个月内下降了 70% 以上。

这种进攻性 AI 能力的指数级增长意味着旧的安全模型——聘请审计师、获取报告、部署、祈祷——在结构上是不足的。a16z 框架通过建立一种以规范（specification）的速度而非人工代码审计的速度进行进化的防御体系来解决这一问题。

AI 也在赋能防御端。Certora 的 AI Composer 于 2025 年 12 月发布 Alpha 版本，是第一个将形式化验证（formal verification）直接集成到代码生成过程中的 AI 编程平台。专用 AI 安全代理在受控研究中展示了 92% 的漏洞检测率。2026 年的审计并非完全自动化，而是由 AI 分析辅助的人类专家，在更短的时间内覆盖 10 倍以上的代码。

现实世界的应用：谁在这样构建？

从理论到实践的转变已经在进行中。

Aave V4 代表了 DeFi 历史上最全面的分层安全实现。该协议的安全审查历时约一年，从 2025 年初持续到 2026 年 2 月，预算经 DAO 批准达 150 万美元。Certora 从最早的设计阶段就开始与开发人员合作，进行形式化验证和不变量测试，而 ChainSecurity、Trail of Bits 和 Blackthorn 则进行了多轮人工审计。结果是：一个在部署前通过数学方式验证安全属性、并在部署后持续监控的协议。

Kamino Finance 在 Solana 上开始使用 Certora Prover 检查关键不变量，捕获了可能导致抵押品超额赎回的精度损失漏洞——这正是人工审计师历史上经常遗漏的极端情况。

Sui 生态系统 在语言层面采用了形式化验证，Sui Prover 已开源，将曾用于飞行控制系统和处理器设计的数学验证技术带到了 Move VM 上的日常智能合约开发中。

Guardrail 正在将生产协议的运行时强制执行（runtime enforcement）投入运营，将理论上的“断路器”概念转化为保护真实资产的部署基础设施。

仍然存在的差距

尽管取得了进展，但一个关键差距仍然存在。目前还没有全球性的要求规定高 TVL（总锁定价值）协议必须运行持续的对抗性测试、运行时强制执行或代理感知监控。一个协议仍然可以在没有运行时强制执行的情况下发布，而用户仍然会根据一份审计 PDF 和一个认证图标存入数十亿美元。

保险市场可能会迫使自愿采用未能实现的改变。随着 AI 驱动的漏洞发现变得更加容易获得，保险协议开始要求将 AI 监控作为承保的前提条件。Bug 赏金平台正在集成 AI 代理作为初审员。经济逻辑很简单：如果 AI 能够以 1.22 美元的成本发现漏洞，那么不运行防御性 AI 的代价将是天文数字。

尽管 TVL 在增长，但 2025 年底 DeFi 被黑损失有所下降，这表明了显著的进步。Chainalysis 指出这是“与早期周期的关键分歧，早期周期中 TVL 的上升通常意味着更多成功的攻击”。但威胁正在演变。朝鲜的 TraderTraitor 组织已从协议漏洞转向云基础设施攻击。社会工程学现在已超越智能合约漏洞，成为加密货币的主要攻击媒介。安全周界正在扩张，虽然智能合约的形式化验证是必要的，但还不够。

“规范即法律”对 DeFi 未来意味着什么

a16z 的愿景一旦完全实现，将从根本上改变部署 DeFi 协议的意义。在启动之前，每个关键安全属性都将经过形式化证明——不是测试，不是审计，而是在所有可能条件下经数学证明成立。启动后，运行时护栏将实时强制执行这些属性，自动回滚任何威胁协议完整性的交易。

这不是“快速行动，打破常规”。恰恰相反：精确行动，并证明没有任何东西会损坏。这种方法模仿了航空和半导体行业处理安全的方式——通过形式化方法，不给“我们认为它可行”留下任何空间。

2026 年的 DeFi 安全格局正在分化。一边是：将安全视为勾选框的协议，依赖特定时间点的审计，并希望 AI 驱动的攻击者找不到人工审计师遗漏的漏洞。另一边是：将安全性嵌入其架构的协议，使用形式化验证和运行时强制执行，使整类漏洞在结构上变得不可能发生。

2025 年损失的 34 亿美元是旧方法的代价。“规范即法律”框架是 a16z 的赌注，赌这个行业能够——而且必须——做得更好。

---

在区块链基础设施上构建需要你可以信任的基础。BlockEden.xyz 提供跨 Ethereum、Sui、Aptos 以及 20 多个链的企业级 RPC 和 API 服务——这是注重安全的开发人员所需的可靠基础设施。探索我们的 API 市场，在专为持久性设计的基础上进行构建。