你用 Codex 或 Claude Code 让 AI 帮你写了一个复杂的支付模块。代码看起来没啥问题，测试也通过了，你就放心地合并了。两周后，一个边缘 case 触发了隐秘的 bug，导致部分用户的余额被重复扣除。你翻回去看那次对话记录，试图搞清楚 AI 当时到底是怎么想的，但聊天日志里只有一段模糊的描述和几轮来回修改。

这不是什么虚构的场景，这是每个深度使用 AI 编程工具的开发者都在面对的现实。

AI 编程的信任危机#

过去一年里，「Vibe Coding」席卷了整个开发者社区。你不需要深入理解每一行代码，你只需要描述你想要什么，AI 就会吐出能跑的代码。效率提升是真实存在的，Codex 和 ChatGPT Work 的日活用户从 600 万跳到 700 万只用了 24 小时，这个数字本身就说明了一切。

但效率提升的背后，我们丢掉了一个至关重要的东西：对代码的信任。

在 AI 时代之前的软件工程流程是这样的：需求 → 架构设计 → 详细设计 → 编码 → 测试 → 代码审查 → 部署。每一步都有明确的输入、输出和人类负责人。我们信任软件，是因为我们信任这个流程。即使不能数学上 100% 证明代码没有 bug，我们也确信它经过了多层人工审查和自动化测试。

到了 AI 时代，这个流水线被压扁了。你输入一个 prompt，AI 直接输出可运行代码，中间环节全部消失。虽然我们试图用 prompt engineering 和自动化测试来追赶，但从用户提示到最终代码的路径依然是一个黑箱。

问题具体表现在四个方面：

第一，AI 行为不可预测。 代码来自千亿参数的神经网络，我们无法完全理解或预测。完全相同的 prompt 可能产生底层完全不同的代码。

第二，bug 难以溯源。 AI 代码出问题时，你很难把故障追溯到某个具体的设计缺陷或逻辑错误。你不知道是 prompt 的问题、模型的问题、还是上下文的问题。

第三，修复不可控。 让 AI 修一个 bug 的时候，它可能在你完全不知情的地方引入了副作用。修一个，坏三个，这是 AI 编程的经典困境。

第四，人工审查已不可能。 人类根本不可能以 AI 生成代码的速度进行 review。代码审查正在变成一种走形式的 checkbox 操作，失去了它本该有的质量把关意义。

传统的验证方法为什么不够用#

计算机科学家们尝试用形式化方法（Hoare 逻辑、Z 语言、模型检查等）来验证程序正确性已经几十年了。但它们的共同问题是：它们关注的是「发现问题」，而不是「把事情做对」。

传统验证方法试图在代码写完之后再去证明它是正确的。这本质上是被动的，而且极其困难。你需要在写完所有业务逻辑的 if/else、数据库调用和 try/catch 之后，再去证明它们之间没有冲突，这是一个接近 NP-hard 的问题。

更不用说状态爆炸问题：验证大型程序需要检查天文数字级别的可能路径，即使是最好的验证工具也会被瞬间压垮。

语义合约：换个思路解决问题#

面对这个困境，一篇发表在 Substack 上的技术文章提出了一个有趣的思路：语义合约（Semantic Contracts）。

核心想法很简单：我们不要在代码写完之后再去「验证」它是否正确，而是让正确性成为构建过程的自然副产品。

语义合约是什么？它可以被理解为一种结构化的、可验证的蓝图，放在人类需求和实际代码之间。它用类型化的状态（States）、简单的组合器（Combinators）和编译期检查来保证：只要实现符合合约的定义，它就是可信的，不管这个实现是人写的还是 AI 生成的。

一个语义合约由三部分组成：

  • 签名（Signature）：定义什么状态输入，什么状态输出。比如 contract Payment(AccountId, Money, OrderId) : Success | InsufficientBalance | Failed
  • 骨架（Skeleton）：用基础的组合器构建表达式树。比如 Seq<A, B> 表示先执行 A 再执行 B，Par<A, B> 表示并行执行 A 和 B
  • 能力（Capability）：附加数据库事务、重试、限流、日志等行为

这里的关键创新是：合约不抛异常，而是返回显式的「状态」。比如支付操作可能返回 Success(TransactionId)、InsufficientBalance(available: Money) 或 Failed(Error)。如果下一个步骤没有显式处理 InsufficientBalance 这个状态，编译器会直接报错，强制开发者（或 AI）在代码运行之前就处理完所有边缘情况。

这跟 Rust 的 Result 类型有点相似，但范围更广。它不是语言层面的错误处理，而是把整个业务逻辑变成了一个类型系统。

用排序算法来理解#

以快速排序为例，用语义合约的方式可以这样定义：

首先定义「可信基础工具」（原子操作）：

  • CheckSorted：检查列表是否已排序
  • Partition：按 pivot 分成「小于」和「大于」两部分
  • Merge：合并两个已排序列表

然后用组合器把它们串起来：

  • 先检查是否已排序（处理空列表和单元素列表的边界情况）
  • 如果没有，则分区 → 递归排序 → 合并

对于纯数学问题（比如排序），合约本质上就是算法本身。但对于业务应用，合约的作用更偏向于「约束」而不是「实现」。

电商结账系统的实战例子#

来看看一个真实的电商结账场景。传统代码里，支付和库存的业务规则被埋在嵌套的 if/else、数据库调用和错误捕获块中。没有任何自动化的方式来证明它们之间不会互相冲突。

用语义合约的方式，你可以把「下单」分解成几个独立的状态流转：

Payment: 账户余额检查 → 扣款 → 返回 Success 或 InsufficientBalance
Inventory: 库存检查 → 扣减 → 返回 Success 或 InsufficientStock
PlaceOrder: Seq<Payment, Inventory>

当 Payment 返回 InsufficientBalance 时，编译器会强制 PlaceOrder 层必须处理这个状态（比如发邮件通知用户充值），否则编译不过。整个业务流程变成了一个有向无环图（DAG），每一步的状态转换都被类型系统严格约束。

这对 Codex 用户意味着什么#

你可能会问，这跟 Codex 有什么关系？

关系太大了。Codex 本质上就是一个在对话中生成代码的 agent。它当前的模式是「对话驱动」的：你说需求，它写代码，跑测试，修错误，循环往复。你在旁边盯着看的时候，它表现得很好；但当你把它丢去独立执行长时间任务的时候，信任问题就暴露出来了。

语义合约的思路暗示了一个可能的未来方向：Codex agent 在动手写代码之前，先生成一个结构化的执行计划（合约），你审核确认后，它再按合约的约束去实现。 这样，你的代码审查就从事后阅读 diff 变成事前审核蓝图，AI 的自由度被类型系统框定在一个安全的范围内。

这不只是理论。实际上，Terraform 就是这个理念在基础设施领域的成功案例。没人会用 agent 循环的方式去管理基础设施（「我给你一个关于基础设施的 prompt，你自己一步步试」）。大家用的都是 terraform plan → 审核 DAG → terraform apply。AI 编程工具完全可以借鉴这个模式。

总结#

AI 编程的效率红利是真实的，但我们不能为了速度牺牲可信度。语义合约不是银弹，它解决不了所有问题（比如原子操作本身的正确性依然需要单元测试来保证），但它提供了一个有趣的方向：用类型系统和编译期检查，把「信任」从人类审查的主观判断，变成编译器可以自动验证的客观约束。

代码会被重写、重构、替换，但架构层面的约束才是持久的东西。当 AI 生成的代码量以指数级增长的时候，唯一可持续的策略，就是让架构本身成为质量的门禁。

参考来源：Beyond Vibe Coding: Rebuilding the Broken Chain of Trust with Semantic Contracts by bz, Jul 17, 2026