Sui Prover 正式开源：为什么形式化验证是智能合约安全中缺失的一环
2025 年，尽管大多数受攻击的协议都经过了审计，甚至有些还审计了多次，DeFi 仍因智能合约漏洞损失了 33 亿美元。2 月份发生的 15 亿美元 Bybit 攻击、4200 万美元的 GMX 漏洞以及无数次重入攻击，证明了一个令人不安的事实：传统的安全审计是必要的，但并不充分。当数学精度至关重要时，仅仅测试极端情况是不够的。你需要证明它们。
这就是 Sui Prover 开源的意义，它远比仅仅在 GitHub 上发布一个项目更重要。Sui Prover 由 Asymptotic 开发，现在免费提供给 Sui 开发者社区。它将形式化验证（Formal Verification）引入到日常的智能合约开发中。这种数学技术同样被用于确保飞行控制系统和处理器设计不会失效。在这样一个哪怕一个被忽视的边缘情况都可能导致数亿美元损失的背景下，通过数学方式证明代码行为正确已不再是一种奢侈，而正成为一种必需。
审计悖论：当 “安全” 还不够安全时
2025 年的区块链安全格局暴露了一个令人担忧的模式。根据 Halborn 的《前 100 名 DeFi 黑客攻击报告》，即使通过了严格审计的协议仍然沦为漏洞利用的受害者。原因各异：供应链漏洞、访问控制缺陷、经济模型中微妙的数学错误。但共同点是，传统的代码分析——无论是人工审查还是自动化扫描——都无法捕获所有可能的故障模式。
以 Yearn yETH 的 Bug 和 Balancer 的舍入误差漏洞为例。这些并不是业余错误，而是微妙的数学误差，它们在成千上万条潜在的执行路径中利用了舍入精度。审计员可能花费数周时间审查代码，但仍可能错过那个触发灾难性行为的特定输入组合。
GMX 漏洞展示了问题的另一个维度。漏洞并不存在于核心交易逻辑中，而是出现在组件之间的边界，即预言机与保证金计算交汇处，以及清算逻辑与桥接基础设施交互的地方。当故障源于组件之间的交互时，仅测试单个组件是不够的。
这正是形式化验证与传统安全方法有本质区别的地方。形式化验证不是检查特定的测试案例，而是通过数学证明某些属性在所有可能的输入和执行路径下都成立。如果你能证明一个保险库在任何情况下都不会被搬空，你就无需担心测试中错过的隐蔽边缘情况。
形式化验证究竟在做什么
形式化验证将代码转化为数学陈述，然后证 明这些陈述与预期行为的形式化规范相匹配。其过程如下：
首先，开发者编写规范（Specifications）来描述他们的代码应该做什么——不是使用编程语言，而是使用专门为表达数学属性而设计的规范语言。对于智能合约，这些规范可能包括诸如 “除非调用铸造（mint）或销毁（burn），否则代币总供应量永远不会改变” 或 “用户余额只能在获得用户明确授权的情况下减少” 等陈述。
然后，验证器工具——在本例中是基于 Boogie 验证引擎和 Z3 SMT 求解器构建的 Sui Prover——会详尽地检查代码在所有可能的输入下是否满足这些规范。与检查特定值的测试不同，验证器通过数学推理同时评估所有可能的输入。
当验证成功时，你就拥有了指定属性成立的数学证明。当验证失败时，验证器通常会提供一个反例——一个会违反规范的特定输入，这通常会揭示出测试可能会错过的 Bug。
Sui 和 Aptos 所使用的 Move 编程语言，从一开始就是为了形式化验证而设计的。其面向资源的模型和强静态类型提供了一个基础，使得形式化验证比 Solidity 等语言更具实践性。Move 规范语言（MSL）允许开发者表达三类属性：
- 结构体不变性（Struct Invariants）：结构体在其整个生命周期内应保持的状态。
- 函数规范（Function Specifications）：每个函数的前置条件、后置条件和行为保证。
- 全局状态规范（Global State Specifications）：在所有状态转换中必须保持的系统级属性。
Sui Prover：从内部工具到社区资源
Asymptotic 最初开发 Sui Prover 是为了支持他们在 Sui 协议上的审计工作。作为 Sui 上唯一的形式化验证提供商，他们需要能够超越人工审查、以数学方式验证客户代码库高风险区域的工具。
开源该工具的决定既反映了形式化验证技术的成熟，也反映了安全是一种公共利益的共识。当更多开发者能够使用形式化验证时，整个生态系统都会变得更加安全——这将使所有人受益，包括能够专注于更高级别问题的安全审计员。
Sui Prover 可以在 GitHub 上找到，并可通过 Homebrew 安装（brew install asymptotic-code/sui-prover/sui-prover）。开发工作仍在积极进行中，2026 年 1 月提交的最新议题涉及持续的改进。
使 Sui Prover 具有极高价值的是它与 Sui Move 现有开发工作流程的集成。开发者可以增量地向现有代码添加规范，先验证关键函数，然后逐渐扩大覆盖范围。这些规范既可以作为安全检查，也可以作为文档——任何审查或集成合约的人都可以通过阅读规范来了解受保证的行为。
你可以证明的真实场景属性
当你考虑到可以证明的具体属性时，形式化验证（Formal Verification）的力量就变得具体可见：
不可被排空的金库：对于持有用户资金的 DeFi 协议，证明任何操作序列在未经适当授权的情况下都无法排空金库，从而消除了整类攻击。这并非“我们测试了许多攻击向量”——而是从数学上确定 排空金库是不可能的。
不会下降的份额价格：收益金库和流动性池通常需要保证份额价格永远不会意外下降（在预期滑点之外）。形式化验证可以证明，无论市场条件或用户行为如何，这一属性都成立。
精确的余额保留：代币合约可以证明总供应量在所有操作中保持不变，转账移动的正是指定的金额，并且除了通过指定函数外，不会创建或销毁任何代币。
访问控制保证：证明只有获得授权的地址才能调用特权函数，无论合约处于何种状态或之前的操作序列如何。
经济不变性：复杂的 DeFi 协议可以证明其经济模型的属性——流动性约束得到遵守、抵押率得以维持、套利循环无法提取无限价值。
这些并非理论案例。Sui 生态系统中的开发者已经应用形式化规范来验证 DeFi 合约，包括 AMM 和杠杆收益耕作系统。当这些属性是被证明而不仅仅是假设时，安全态势将发生根本性变化。
安全格局需要更好的工具
2025 年的统计数据使形式化验证的理由极具说服力。根据安全研究人员的说法，在 2024 年，链下事件占攻击次数的 56.5% 和资金损失的 80.5%，但智能合约漏洞在被利用时仍然具有毁灭性。仅访问控制漏洞就在整个 2024 年造成了 9.532 亿美元的记录损失。
2025 年的 OWASP 智能合约前十大风险（Smart Contract Top 10）记录了去中心化生态系统中超过 14.2 亿美元的总损失。传统的安全工具——用于符号执行的 Mythril、用于基于属性的模糊 测试的 Echidna，以及来自 OtterSec、Halborn 和 MoveBit 等公司的手动审计——解决了问题的不同方面。但随着协议变得更加复杂并处理更多价值，这些方法之间的差距变得更加危险。
CertiK 已部署形式化验证技术来对智能合约进行数学验证，根据其报告，保护了超过 3000 亿美元的资产。这一规模既展示了对数学安全保证的需求，也展示了将形式化方法应用于区块链系统的可行性。
安全研究人员中新出现的共识是，审计、漏洞赏金、监控、逐步发布和形式化方法应作为多层防御共同发挥作用。对于高价值系统，关键不变式的形式化验证正成为行业标准做法，而非例外的严苛要求。
为什么 Move 让形式化验证变得切实可行
并非所有编程语言都同样适用于形式化验证。Solidity 的灵活性和 EVM 的复杂性使得形式化验证具有挑战性——虽然可行，但需要大量的工具开销和专业知识。
Move 的设计初衷则完全不同。其面向资源的模型意味着资产具有线性类型（Linear Types），不能被隐式复制或丢弃。类型系统在编译时捕获了整类在其他语言中需要运行时检查的漏洞。Move Prover 与该语言同步开发，确保了语言特性与验证能力之间的紧密结合。
这种设计传承意味着 Move 标准库本身经过了形式化验证。当你在 Sui 或 Aptos 上构建时，你是在一个拥有正确性数学证明的基础上进行构建——随着你将自己经过验证的代码叠加在上面，这些证明会产生复利效应。
实际意义在于：Move 上的形式化验证比其他平台需要的专业知识更少。Sui Prover 的文档、示例以及与标准开发工作流程的集成，使得非形式化方法专家的开发者也能使用它。你可以循序渐进地学习编写规范，从简单的函数合约开始，随着理解的深入逐步过渡到复杂的不变式。
这对 Sui 开发者意味着什么
对于在 Sui 上构建的开发者来说，开源的 Sui Prover 创造了新的可能性：
安全差异化：在竞争激烈的 DeFi 领域，证明安全属性不仅是降低风险，更是一种竞争优势。用户和审计员可以验证有关协议安全性的声明，而不是仅仅相信断言。
降低审计成本：当关键函数拥有形式化证明时，审计员可以专注于更高层面的关注点，而不是穷举测试边缘案例。这可以减少审计范围和成本，同时实际上提高安全结果。
文档质量：形式化规范是不会过时的精确文档。当规范声明某个函数保持特定的不变式时，这要么是可证明的真理，要么验证器会标记违规。
渐进式采用：你不需要形式化验证所有内容。从风险最高的函数开始——例如处理提现、抵押或特权操作的函数——并随着时间的推移扩大覆盖范围。
Sui 生态系统已经拥有多家经验丰富的审计公司，包括 MoveBit（Move 形式化验证的先驱）、Certora、OtterSec 和 Zellic。Sui Prover 增加了一个开发者可以直接使用的工具，而不必为每一项验证任务都聘请外部审计。
更广泛的发展轨迹
Sui Prover 的开源符合整个区块链行业安全工具成熟化的宏观趋势。形式化验证正在从学术研究转向生产基础设施，从专门的咨询服务转向开发者触手可及的工具。
这一轨迹至关重要，因为智能合约所保护的价值规模在不断增长。DeFi 协议集体管理着数千亿美元的资产。一个主要协议中的单一漏洞造成的损失，可能超过传统软件公司在其整个存续期间面临的损失。
传统软件行业最终在航空电子、医疗设备、金融系统等安全关键系统中采用了形式化方法。在“代码即法律”且漏洞通常不可逆转的区块链行业，拥抱数学验证的理由更为充分。
Sui Prover 代表了向这个方向迈出的一步：让形式化验证变得足够易用，使开发者能够真正地去使用它，而不是将其束之高阁，变成无人问津的安全虚假宣传文档。
快速入门
对于有兴趣在 Sui 上探索形式化验证的开发者：
- 安装 Sui Prover：
brew install asymptotic-code/sui-prover/sui-prover - 从细微处着手：为一个关键函数添加规范并验证其通过
- 学习规范语言：Move Specification Language 拥有出色的文档，用于表达常见属性
- 迭代：随着信心的建立，将覆盖范围扩展到更多函数和更复杂的不变量
在学习形式化规范方面的 投入会产生复利效应。一旦你验证了底层模块是正确的，你就可以在确信这些基础已通过数学证明的情况下，构建更高级别的逻辑。
对于一个在 2025 年因可预防的漏洞损失了数十亿美元的行业来说，问题不在于形式化验证是否值得投入。问题在于生态系统能以多快的速度采纳它。Sui Prover 的开源发布消除了一个障碍——现在需要跟上的是知识和实践。
在 Sui 上构建安全的应用程序需要与你的协议安全标准相匹配的可靠基础设施。BlockEden.xyz 为 Sui、Aptos 以及 20 多个链提供企业级 RPC 端点，具备生产级应用所需的运行时间和可靠性。探索我们的 API 市场，为你经过形式化验证的智能合约提供动力。