AI生成代码的隐性风险：我们正在交付看不见的假设

代码看起来没问题。lint 通过了，浅层的测试也过了。大家都——凭感觉——认为我们做对了。

然后，边界情况在生产环境出现了。

开发者把它当作正常的操作流程：bug 会有的，工单会来的，补丁会发的。QA 被问为什么没有发现它。但 QA 从来没有收到系统的模型——只有一份充满假定的实现，被期望去反向工程。

这就是 AI 辅助开发中越来越常见的失败模式。我们生成代码的速度超过了理解它所创建系统的速度。危险不再局限于一个坏函数或一个明显的语法错误。它存在于组件之间的空间：边界、状态转换、失败模式和不变式。

我们不只是在交付代码。我们交付的是已经看不见的假定。

整洁的代码不是连贯的系统

Linter 可以告诉我们代码是否遵循一组局部规则。测试可以告诉我们选定的例子是否产生预期的结果。两者都无法告诉我们系统必须保留什么，除非有人先声明它。

不变式是这类声明之一：它是一个必须在系统每个有效状态下始终保持为真的条件。账户余额不能在没有相应交易的情况下被修改。私有对象不能在未经授权的情况下变成公开的。两次成功的写入不能悄无声息地相互覆盖。

当不变式保持隐式时，整洁的代码仍然可以组装成一个不连贯的系统。每个组件单独看可能都是合理的，而失败正等待在转换、重试、竞态或没人想到要画的边界中。

那就是 AI 辅助开发正在迅速用代码填满的空间。

没有黄金时代——那时候每个开发者在碰编辑器之前都会写一份正式的规格说明。大多数团队没有这样做过。早期的软件也满是隐藏的假定，怀旧情绪有一种习惯，会把过去不便利的部分抹去。

但这个领域确实发展出了在代码之上进行推理的学科：架构模型、状态机、形式规格说明、模型检查、故障注入和确定性模拟。我们倾向于把它们留给那些失败明显代价高昂的系统。在其他地方，严格性被视为要最小化的成本。

然后实现变得便宜了。框架隐藏了机制。包把多年的专业知识压缩成一次导入。这带来了巨大的好处，但也使得构建系统而不必看透其表面成为可能。

生成式 AI 加速了同样的权衡。它可以在团队尚未就系统是什么达成一致之前就产生一个看似合理的实现。当没有人将那个意图外化时生成的代码就变成了默认的设计。QA 在下游承受后果。

缺失的那一层不是更多的代码审查。它是Human Intent和Machine Output之间的共享模型。

三个模型，三个问题

没有任何单一技术能覆盖那一层。一个有用的栈需要回答三个不同的问题。

1. C4：存在什么，它们如何关联？

C4 模型为软件团队提供了一种可视化系统的层次结构：上下文、容器、组件和代码。它像一张有缩放级别的地图。在最宽的视图，我们看到系统、它的用户和相邻的系统。放大则揭示应用程序、数据存储、服务、组件和关系。

关键不是为每个项目制作四张强制性的图表。官方指南指出，上下文图和容器图对许多团队来说已经足够。关键是要让边界变得可以讨论。

这很重要，因为生成的代码具有局部说服力。一个服务可能看起来完整而其所有权不明确。一个 API 可能看起来整洁而其信任边界不可见。C4 给开发和 QA 在任何一方不得不从仓库推断系统之前提供相同的结构地图。

AI 可以帮助从需求或现有代码库起草那张地图。它不应该有最终决定权。人类仍然需要问地图描述的是否是他们打算运营的系统。

2. TLA+：什么可能发生，什么必须保持为真？

C4 显示结构，但仅有结构无法表达行为。它不能告诉我们哪些状态是有效的，哪些转换是允许的，或者哪些条件必须在每次交错中存活。

这就是 TLA+ 的用武之地。Leslie Lamport 将其描述为一种用于在代码级别之上构建精确高层模型的语言，特别适用于并发和分布式系统。它的 TLC 模型检查器可以探索行为并找到违反我们声称应该保持的属性的痕迹。

TLA+ 强制进行一场不同的对话。不是问"这个函数有效吗？"而是问："系统从这个状态可以做什么，每个可达结果都是可接受的吗？"

符号可能是正式的，但 AI 可以降低入门成本：起草初始规格说明，将自然语言承诺翻译成候选不变式，解释反例trace，帮助团队完善模型。人类的工作是决定这些承诺是否真的正确。形式化了错误意图的模型只是在错误的系统上变得精确。

3. DST：实现是否遵循模型？

一个正确的模型不能证明生产代码正确实现了它。我们仍然需要实现能够反驳。

确定性模拟测试，或称 DST，在受控世界中运行真实实现代码。时间、随机性、调度、网络、存储和故障都成为模拟器可以操作的输入。当生成的场景导致失败时，它的种子使运行可复现。

TigerBeetle 的 VOPR 是一个引人注目的例子。它可以在一根线程上模拟集群、加速时间并注入存储故障。TigerBeetle 在其架构文档中做了一个重要的区分：模型检查可以暴露算法中的错误，而模拟则练习特定的实现及其底层假定。

这三层相互补充：

C4 映射系统。TLA+ 声明什么必须保持为真。DST 试图使其为假。

一个针对富饶代码的工作流

这不需要成为团队维护大量图表和规格说明的新仪式——那些图表和规格说明会立即过时。模型必须参与工程循环。

用自然语言声明承诺。在生成实现之前，写下系统必须始终保留什么，以及它必须永远不允许什么。

用自然语言声明承诺。在生成实现之前，写下系统必须始终保留什么，以及它必须永远不允许什么。

画出边界。使用 C4 来识别用户、外部系统、容器、组件、数据存储，以及假定从一个所有者跨越到另一个的关系。

画出边界。使用 C4 来识别用户、外部系统、容器、组件、数据存储，以及假定从一个所有者跨越到另一个的关系。

为风险行为建模。在并发、排序、重试、权限或状态转换使承诺难以非正式推理的地方使用 TLA+。

为风险行为建模。在并发、排序、重试、权限或状态转换使承诺难以非正式推理的地方使用 TLA+。

从经过审查的意图生成。只有在人们挑战了结构和行为模型之后，才让 AI 生成实现和测试。

从经过审查的意图生成。只有在人们挑战了结构和行为模型之后，才让 AI 生成实现和测试。

确定性攻击实现。把有风险的依赖——时间、随机性、调度、网络或存储——置于控制之下。生成恶意场景，保留它们的种子，重放每个失败。

确定性攻击实现。把有风险的依赖——时间、随机性、调度、网络或存储——置于控制之下。生成恶意场景，保留它们的种子，重放每个失败。

将现实反馈到模型中。生产观察和模拟失败揭示了团队错过的假定。更新不变式，然后更新实现和测试。检测漂移而不是允许模型成为历史的装饰。

将现实反馈到模型中。生产观察和模拟失败揭示了团队错过的假定。更新不变式，然后更新实现和测试。检测漂移而不是允许模型成为历史的装饰。

不是每个应用都需要像 VOPR 那样复杂的模拟器或大型 TLA+ 规格说明。轻量级版本可能是一张上下文图、一张容器图、五个书面不变式、一个针对最冒险转换的小模型，以及围绕它的一个有种子测试工具。

目标不是最大程度的正式化。目标是给每个重要假定一个地址。

一切对某人都至关重要

想象一位祖母用 AI vibe-coding 一个家庭相册。这不是财务账本或飞行控制系统。但这个应用做出了真实的承诺：

原始照片绝不能被销毁。

私人照片绝不能意外暴露。

说明文字和时间顺序必须在每次编辑中存活。

两个家庭成员不能相互覆盖对方的更改。

她的 C4 模型可以很小：一个人、一个应用程序、一个身份提供者、本地存储、云存储和一个共享边界。她的 TLA+ 模型不需要描述整个产品；它可以专注于并发编辑、删除或权限。确定性工具可以模拟两个设备离线、编辑同一个相册、以不同顺序重新连接并重试中断的上传。

这一栈曾经与任务关键工程相关联，因为严格是昂贵的。但 AI 改变了经济学。如果实现现在几乎免费地到来，为什么严格应该仍然是奢侈品？

关键性不是由基础设施规模决定的。它是由失败对信任这个系统的人的后果决定的。

一切对某人都至关重要。

检索，不是撤退

把软件历史讲述为简单的堕落是很诱人的：曾经我们理解了机器，然后我们专门化了，然后我们配置包了，现在我们提示模型为我们做那些。

这个故事在情感上可辨认，但在历史上不完整。现代开发者并非不那么聪明，抽象也不是敌人。更深层的问题是宝贵的学科变得埋葬在便利之下。我们保留了输出，却失去了产生它们的一些推理的接触。

这就是怀旧可以有用的地方。不是作为重建想象中过去的要求，而是作为诊断信号。它告诉我们当下有些东西变得难以看到或珍视。

计算机科学给我们留下了面包屑：C4、TLA+、状态机思维、确定性模拟器、小型可组合工具，以及数十年的系统文献。AI 可以帮助挖掘那份遗产。它可以解释不熟悉的符号，从旧代码中恢复架构知识，起草模型，生成工具，并使专业技本对普通团队变得可接近。

那是检索，不是撤退。

更快的代码生成的答案可能是更古老、更深层的建模。

人类拥有承诺

共享模型也修复了一种组织失败。

没有它们，开发者交给 QA 的是一份充满隐式决策的实现。QA 运行它能看到的检查。边界情况到达生产环境，组织问为什么测试错过了它。假定向下游移动，责备也随之移动。

有了结构地图和显式不变式，QA 不再需要猜测开发者是什么意思。测试人员可以挑战承诺，识别缺失的状态，设计恶意场景，并将新发现反馈到模型中。质量成为共同的推理行为，而不是最后排队团队运营的最终关卡。

这恢复了一种 AI 无法为我们生成的人类价值。我们的价值从来不只是在于输入每一行代码。它在于决定一个系统是为了什么，认识到谁可能受到伤害，使其承诺可见，并在承诺被打破时承担责任。

更少的人应该能够通过说"AI 写的"来Dismiss一个失败。

生成不转移责任。如果我们已经决定了系统是为了什么，接受它的输出，并将其发布到某人的生活中，它打破的承诺仍然是我们的。

AI 可能产生代码。人类拥有承诺。

Disclosure: This article was developed with AI assistance through an iterative editorial process. The argument, examples, editorial direction, and responsibility for accuracy remain with the human author.