DeFi 已经进入了它的下一个阶段——一个安全写入每个链、协议和交易所 DNA 的时代。
2025 年，该行业达到了 2.5 万亿美元的链上价值。但成功孕育着风险。新的漏洞、攻击途径和差距在区块链生态系统的安全态势中暴露出来。在这个关键时刻，各公司已经认识到，安全不仅仅是在启动前识别错误，而是要确保系统在不断发展和扩展以支持用户不断变化的需求时，仍然保持安全。
Certora 不仅仅是跟上步伐。我们已经证明自己是 DeFi 所需的合作伙伴。
去年，我们的安全足迹扩展到新的链、语言和基础设施层。
我们的安全研究团队规模扩大了四倍。
而且我们的工作也突出了长期安全伙伴关系的重要性。
下面的数字讲述了这个故事：不仅是我们 2025 年所保障的，而且是 Certora 和整个 DeFi 走向安全新世界的势头。
我们受到顶级的信任。你会在哪里着陆？
2025 年，我们扩大了作为 DeFi 大多数最重要协议的安全合作伙伴的角色。在 TVL 排名前 20 的协议中，有 14 个，在排名前 10 的协议中，有 7 个依赖我们，不仅用于一次性审计，还用于持续的、长期的安全合作。
按 TVL 排名，前 20 名中的 70% DeFi 协议都是 Certora 的客户。
前 10 名中的 70% 在持续的、长期的基础上与 Certora 合作。
哪些平台持续与我们合作？
Aave: 5 年以上
Compound: 5 年以上
Sky: 4 年以上
Morpho: 4 年
Silo: 4 年
Safe: 3 年以上
EigenLayer: 3 年以上
Lido: 3 年
Stellar: 2 年
而这仅仅是列表的顶部。还有几十家公司依靠我们来保护他们的平台。仅在 2025 年，就有 44 个新的协议 与 Certora 建立了安全合作关系，包括 Fluid、Jito、Navi、Polygon、Suilend 等等。
这就是为什么去年我们保护了 1965 亿美元 的资产。
规模化安全
现代协议并非存在于单一链或语言上。2025 年，我们审查了整个 web3 领域的数十万行代码 (LOC)：
- EVM: 200,700 LOC
- Solana: 206,600 LOC
- Sui: 33,000 LOC
- Aptos: 16,300 LOC
- NEAR: 6,000 LOC
- 区块链基础设施: 90,000 LOC
- 移动应用程序: 14,000 LOC
- 链下系统: 36,000 LOC 用于 EigenLayer Hourglass, SafeNet, Cork, Lido 工具等等
我们已经解决了每种环境和每种执行模型。我们已经纠正了故障模式和开发人员的陷阱。这是因为安全意味着理解系统在压力下的行为方式，而不管特定的链、语言或时间范围如何。
价值的真正含义
TVL 并不能说明全部情况。Certora 的工作跨越了基础设施层、治理系统和面向用户的应用程序。
- 我们所保护的资产中有 900 亿美元 是通过对协议不变量的设计审查和形式化验证实现的，这意味着正确性经过了数学证明，而不是假设的
- 跨链、执行环境和系统层完成了 150 项审计
- 在部署之前，已识别并防止了 720 多个漏洞
- 99% 的所有发现 在启动前都已由团队修复
- 在发现严重风险后，11 个协议 在部署前被暂停
2025 年的安全不是关于勾选框。而是关于改变结果。
未发生的黑客攻击
2025 年，Certora 识别出：
- 80 个严重漏洞
- 180 个高危漏洞
- 360 个中危漏洞
这些不仅仅是表面问题。它们包括可能导致以下情况的错误：
- 无需利用漏洞即可破产
- 永久冻结用户资金
- 无法清算的债务头寸
- 治理俘获
- 只有在几个月后才会显现的无声经济漂移
在一个案例中，单个协议包含多达 80 个不同的问题，突出了复杂系统在现实条件下可能有多么脆弱。
Certora 还发现了 10 个已部署系统中的实时错误。这再次提醒人们，安全不会在启动时结束，而是需要在市场、使用和链不断发展的情况下进行持续审查。
不断变化的领域
2025 年，我们反复发现并非源于语法，而是源于经济学、假设和跨系统交互的故障。
我们保护了我们的客户免受以下影响：
- 一种可能将有效利率提高至 2,000 倍的数学错误
- Ethereum 的 Fusaka 升级引入的一种微妙的清算失败模式，其中每次交易的 Gas 限制可能会创建无法清算的头寸
- 违反核心不变量（例如份额率单调性）的舍入误差
这些不是可以通过模式匹配捕获的错误。它们需要深入的协议理解、经济推理以及对链级变化的认识。
经久耐用
2025 年，我们的许多工作都集中在确保客户长期的经济偿付能力上。我们的目标是帮助我们的客户构建能够持续存在（数年、数十年甚至更长时间）的协议，并且我们的审计会考虑每次计算的长期影响。通过我们的工作，我们发现了许多会计缺陷，这些缺陷只会在遥远的将来显现，最终引发包括以下在内的灾难：
- 多付利息
- 在没有利用漏洞的情况下打破偿付能力不变量
- 累积永久扭曲系统经济的“幽灵债务”
尽管这些协议在某个时间点的快照中看起来是正确的，但当跨时间检查状态转换时，它们就会失败。
为什么形式化验证是一种保证
协议需要正确性证明，而不仅仅是信心。2025 年，我们的形式化验证流程超越了仅仅检查孤立的功能，而是包括了系统范围的不变量（即必须始终成立的属性）。
以下是我们证明的一些属性：
Aave v4:
• 份额率是单调的
• 用户操作不会使健康的账户变得不健康
• 没有抵押品意味着没有债务
Euler Earn & Kamino:
• 协议偿付能力已得到正式证明
Silo:
• 一致性在供应和提款队列中保持平衡
Stellar:
• 过期的授权不能重复使用
业内最聪明的人
我们的工作只和我们的人才一样出色，我们已经建立了一支深厚的专业知识队伍。2025 年，这支队伍变得更加壮大。
我们将安全研究团队的人数增加了三倍，达到 40 位专家，其中包括 25 位在形式化方法、密码学和系统方面拥有博士学位的人员。
现在我们有四个专门的研究团队。
每个 Certora 审计都由一流的研究人员在团队负责人的监督下进行，并且他们的工作得到形式化验证、自动分析和重复手动审查的支持。我们的研究人员与我们的客户建立深厚的合作伙伴关系 - 跨多个审计、版本和项目进行合作。我们的审计人员在部署及以后始终与我们的客户保持联系 - 审查协议启动、初始化和持续治理的各个方面。
这种级别的安全不是偶然的，而是经过精心设计的。
前进的道路
2025 年取得成功的协议不仅仅行动迅速。他们及早与我们合作，进行了深入的verified，并将安全性视为基础架构，而不仅仅是一个复选框。
Certora 很荣幸能成为这些公司背后的安全合作伙伴，我们对未来的发展感到更加兴奋。
