作者：PaperMoon团队

一、AI 写代码的速度，已经甩开了审计

先说一个让所有区块链工程师都睡不好觉的事实。

2026 年 4 月，一个熟练的 Polkadot 开发者配合 Claude 或 Codex，把一个新 pallet 从零写到可编译，用时不超过半小时。把业务逻辑比较清楚的智能合约迁到 pallet-revive 上，有时只要十几分钟。而一次正式的智能合约审计，哪怕是最轻量的那种，从递交到出报告，一般也要两到三周。重一点的，两三个月。这是一个极其危险的缺口。

过去我们安慰自己说"反正审计成本放在那里，不会有人随便上链"。但 AI 编码代理已经把"写出来"这件事的边际成本压到了近乎零，原本靠价格差筛掉的那部分代码，现在会直接涌进链上。尤其是在 Polkadot 2.0 之后，Agile Coretime 让部署一条应用链像开一个 SaaS 实例一样轻，pallet-revive 又让 Solidity 开发者可以几乎无缝迁过来——代码的供给侧被彻底撑开了。

问题是，需求侧能接得住吗？

链上经济价值依然真金白银，漏洞不会因为你用 AI 写就对你温柔一点。Inferara 这份提案的第一段，没有讲任何技术，只讲了一件事：

"我们把 Claude、Codex 这类 AI 代理的速度，和形式化方法的力量结合起来，让高速开发变得更安全。"

这句话翻译成大白话就是——AI 写得再快，没有数学兜底，都是裸奔。

二、Inferara 到底想做什么：三步走，把形式化验证变成 Skill

这份提案的作者是 0xGeorgii，来自 Inferara 团队。他们正在做一件听起来有点反直觉的事：把"形式化验证"这个长期以来只活在学术论文和航空航天代码里的东西，做成一个普通 Web3 开发者可以直接调用的工具。

整个流程分三步，逻辑其实非常干净：

第一步，开发者写规约

规约（specification）是这套体系里最反直觉的部分。它不是注释，也不是文档，而是用一种严格的约束语言，写下"这段代码应该满足什么数学性质"。比如一个转账函数，规约会规定：总供应量在任何执行路径上都不能变化，发送方余额不能变负，接收方余额不能溢出。

这一步听起来像是把负担从代码转移到规约上了——其实是的。但关键在于，规约的表达力比代码要紧凑得多，而且一旦写对，它就成了一份永久的"合约"，后续无论代码怎么改，只要通过验证，就一定满足这些性质。

第二步，写实现

这一步是最"脏"的一步，也是 AI 最擅长的一步。不管是人类工程师还是 Claude、Codex，可以用 Rust、Ink!、Solidity、以后再加上 RISC-V 上的别的语言，反正把功能写出来就行。写错？不要紧，第三步会替你说实话。

第三步，Inference 做数学验证

Inferara 正在开发的 Inference 是一个开源的语言和编译器，它的任务是接收"规约 + 实现"这两样东西，用形式化的方法证明实现是否在所有可能的输入路径上都满足规约。不是"跑几个单元测试，看起来没问题"，而是数学意义上的"在所有可能的状态下都成立"。

按 Inferara 自己的话说：

"Inference acts as a baseline of the security/implementation correctness."

Inference 是"正确性基线"。这个措辞很克制，但暗含一个相当大的野心——它要成为 Polkadot 生态里所有关键代码的兜底层，不管你上面用什么 AI，不管你用什么语言写的实现，最终都要通过这一层才算数。

三、为什么 JAM 时代特别需要这个东西

这里要插一段背景，否则提案的分量不容易看出来。

Polkadot 正在从 Runtime + Host 的老架构，迁移到 JAM——Join-Accumulate Machine。JAM 最重要的一个改动是把执行层从"只能跑 Substrate Runtime"变成"可以跑任何 RISC-V 字节码"。再加上 pallet-revive 对 EVM 的兼容，理论上 Polkadot 马上要同时承载：

- 原生 Rust pallet
- Ink! 智能合约（Wasm）
- Solidity 合约（通过 pallet-revive 跑在 RISC-V 上）
- 以后可能还有 Move、Cairo 之类的语言生态

这是一个非常诱人的愿景，也是一个非常恐怖的攻击面。

每一种语言、每一套编译工具链、每一个执行环境，都意味着一组独立的漏洞模式。同样一个整数溢出，Rust 里是一种写法，Solidity 里是另一种写法，编译到 RISC-V 之后又是另一种表现。过去我们可以靠"Substrate 就一条路"来简化安全模型，但 JAM 之后，这条假设没了。

Inferara 在提案里讲得很明白：

> "Inference 作为这些不同实现路径之间的统一正确性基线。"

换句话说，他们不是要替代审计，也不是要取代测试，而是要在所有这些语言和执行环境之上，架一层共同的数学语言。不管你底下用什么写、编译到什么，最后都要在这一层上对齐。

这是一个相当大胆的技术判断——JAM 时代的安全问题，不能靠在每一种语言里修修补补解决，必须有一个跨语言的形式化层。

四、Decentration 问出了真正的那个问题

提案下面的讨论区其实比提案本身更有意思。

社区成员 RustSyndicate 问得很具体：LLM 具体怎么接？Rust 和 PolkaVM 兼容不兼容？时间线能不能再细化？这些都是好问题，但本质上还是工程细节。

而 Decentration 的回复，直接把问题拔高了一层。他的观察大意是这样的：

> Polkadot 的 pallet 在源码层面是模块化的，每个 pallet 可以被独立审计、独立推理。但一旦它们被组合进一个 Runtime，编译成 Wasm 或 RISC-V 字节码之后，整个执行单元其实就塌缩成了一个不可验证的单体。跨 pallet 的交互、状态依赖、权限流动，全部糊在一起。而这才是 JAM 协议层真正需要形式化方法的地方。

我觉得这句话值得每一个做 Polkadot 技术架构的人认真读三遍。

因为这指向了一个过去被系统性回避的问题——"模块化"是架构师的叙事，不是验证器的叙事。

我们在画架构图的时候，习惯性地把系统拆成一块一块，假设每一块可以独立分析。但当这些模块被编译到同一个执行环境里共享状态、共享内存、共享权限时，它们就不再是"模块"了，而是一个整体。Runtime 升级曾经出过的那些事故（比如上个月 Hyperbridge 引发的 Runtime v207 中断），本质上都不是单个 pallet 的问题，而是 pallet 组合之后的涌现行为。

Inferara 当前的初版覆盖范围是 SDK、密码学原语、ZK 库——这些都是相对独立、边界清晰的组件。智能合约放在第二轮迭代。但 Decentration 指出的那个"编译后塌缩为单体"的问题，如果真要彻底解决，Inference 迟早要把它的验证能力推到 Runtime 整体甚至 JAM 协议层。

这才是这个工具真正能不能长起来的决定性信号。

五、路线图：克制得几乎让人不安

Inferara 给出的时间表其实非常保守，保守到有点反常。

- 2026 年 3 月：Coding Agent Skill 可用（可以理解为一个能被 Claude、Codex 之类的 AI 代理调用的形式化验证工具）
- 2026 年 4–5 月：稳定版发布
- 2026 年夏季：增强功能
- 初版覆盖：SDK、密码学原语、ZK 库
- 第二轮迭代：智能合约

对比一下生态里其他那些动辄"Q2 主网、Q3 生态爆发"的路线图，这份时间表克制得几乎让人不安。但我倾向于把这种克制当成正面信号。

形式化验证是一个"做不出来就真的做不出来"的领域，没法靠营销话术撑过季度汇报。Inferara 自己也很诚实地承认，目前针对 pallet-balances 的形式化验证研究已经有了阶段性成果，但面向智能合约的生产级 PoC 还没有。他们没有假装自己已经准备好了。

在一个被 vibe coding 填满的 2026 年，这种"先说自己还没准备好"的姿态反而稀缺。

六、这条路的另一面：为什么形式化验证过去一直没普及

当然，要是形式化验证这么好用，它早就被整个行业接纳了。事实是，过去二十年，它基本只活在几个相对封闭的领域——航空航天、核能、心脏起搏器、少数几家投入巨大的金融基础设施。原因主要有三个：

第一，写规约本身是一门手艺。

让一个普通工程师写出正确的规约，难度不亚于让他写出正确的代码。而且规约写错的后果比代码写错更隐蔽——代码写错了还能测出来，规约写错了，整个验证过程会"成功地"证明一件错误的事情。

第二，验证性能曾经是灾难级的。

传统的模型检查器、定理证明器，面对规模稍大的系统往往直接跑不动。验证一个小型 Solidity 合约要几小时甚至几天的情况，一直到 2024 年都不稀奇。

第三，生态里没有人愿意多花这份成本。

在熊市里没人肯为"也许能避免的漏洞"付钱，在牛市里没人愿意等。

Inferara 想用 AI 去同时解决前两个问题——让 AI 辅助写规约、让 AI 参与验证路径搜索——而第三个问题，本质上要靠 JAM 自己把"验证"变成一个不再可选的基础设施动作来解决。这需要整个生态的共识。

这件事能不能成，不只取决于 Inferara 的工程能力，还取决于 Polkadot 社区愿不愿意把"形式化验证"从"锦上添花"提升到"默认动作"。

七、从 Inferara 这件事看 Polkadot 的一个隐线

我一直觉得 Polkadot 这两年的真正主线，不是 JAM，也不是 Agile Coretime，而是一个更底层的方向——从"讲愿景"转向"对自己说实话"。

过去两年我们看到了太多被静悄悄收紧的东西：OpenGov 的权力不再被无节制地下放，Treasury 的支出开始被严格审视，Bloque Stage 3 这种项目提案被明确拒绝，PAPI 的 2026 年资金申请也没通过。生态不再假装每一个方向都值得烧钱。

Inferara 这份提案是这条主线的延伸。它背后的判断其实很朴素：当 AI 把"写代码"变得非常便宜，链上的风险会自动上升，靠旧的审计节奏守不住。

所以 Polkadot 要么继续假装"我们的代码都是一流工程师写的"，要么承认速度已经变了、必须把数学拉进流水线。

这件事如果做得成，Polkadot 会成为第一个把形式化验证做成默认工具的主流 L1 生态。这不一定会立刻带来 TVL 上的暴涨，但会让它在下一轮应用爆发里处于一个非常罕见的位置——"速度 + 可证明性"的那个交叉点。

做不成也没关系。至少它说明这个生态里仍然有人愿意去回应"AI 时代的基础设施到底要具备什么属性"这种真正的第一性问题，而不是满足于再发一个跨链桥的集成公告。

八、结语：不是让 AI 慢下来，而是给 AI 套一层数学

回到提案最开始那句话。

"把 AI 代理的速度，和形式化方法的力量结合起来。"

这句话乍看像标语，仔细看其实是一个非常特定的技术姿态——不反对 AI，不试图把 AI 赶出开发流程，但也不假装 AI 不会出错。

它的哲学是：AI 会出错，人也会出错，所以把"能不能错"这件事交给数学。AI 和人类负责把事情做快、做出来，数学负责说"你这次真的对了"。

这套分工，很可能就是 Web3 基础设施在 AI 时代的正确分工方式。

Polkadot 现在走到一个很微妙的位置：它已经是少数几个正视 AI 会重塑代码供给曲线这件事的主流生态，而 JAM 又恰好在架构上给了它一个足够大的空间去做"跨语言的形式化统一层"。Inferara 只是这条路径上的一个具体提案，后面会不会有更多团队跟进、社区愿不愿意投入 Treasury 资源去支持这个方向、JAM 协议层要不要把形式化接口写进标准——这些都还是悬而未决的问题。

但方向已经清楚了。