Vibe Coding 火了。打开编辑器，用自然语言描述你想要的东西，AI 几分钟就能吐出一个可运行的 demo。这种体验让人兴奋，但兴奋之后你会发现一个问题：demo 能跑，但你敢把它部署到生产环境吗？

一句话能生成一两万行的原型项目，但很难相信它能给你一个承载核心业务的、可增长的软件系统。AI 生成快，也"错得快"——GitLab 2025 年的数据显示，AI 共同编写的代码包含的重大问题是人工代码的约 1.7 倍，逻辑错误高出 75%，安全漏洞高出 2.74 倍。

所以真正值得思考的不是"AI 能不能写代码"，而是"怎么让 AI 写出正确的代码"。这正是 Formal Method 的切入点。

---

速度与正确性：不是二选一

Vibe Coding 解决的是速度问题，Formal Method 解决的是正确性问题。两者不是替代关系，是流水线上的不同工位。

理解这一点很重要。Vibe Coding 的本质是"接受偏差作为速度的代价"——你跟 AI 对话，快速迭代，每次 prompt 和纠正都聚焦于当前关切。但随着迭代进行，一个隐蔽的问题浮现：为了满足新的反馈，AI 经常修改或覆盖之前的决策；之前被隐性声明或松散表达的约束被削弱甚至遗忘。修正变得脆弱——改动一处，别处就引入回归。你最终会陷入一种持续的与 AI 谈判的循环，反复用不同方式重申意图。

根源在于：你脑子里"理所当然"的业务逻辑，从来没有被显式地写下来。AI 不得不猜，而猜的结果取决于你上一条 prompt 的措辞。

Formal Method 做的事情恰恰就是：把隐性的"我想要什么"变成显性的、可检验的约束。不是用来取代 Vibe Coding 的速度，而是给速度装上护栏。

---

Vibe → Spec：两阶段工作流

社区里目前被验证最有效的落地模式是"两阶段法"：先 Vibe，再 Spec。

Vibe 阶段的目标是探索方向。 当 idea 还不清晰的时候，跟 AI 聊，找可行性，定技术栈。这个阶段不急着写代码，重要的输出是一份研究报告或 PRD——哪怕只是一页提纲，覆盖三个基础：你在做什么、给谁用、怎么运转。用推理能力强的模型（比如 DeepSeek R1）来辅助，它会在生成任何代码之前先"思考"数据模型和系统边界。这一步看似慢，实际上会在后续编码时节省大量时间和 token 消耗。

Spec 阶段的目标是保证质量。 拿着研究报告进入 Coding Agent，但不是直接让 AI 开干，而是先让它出一份 proposal——描述要做什么、怎么做、分几步。人 review 通过之后，再按 proposal 写代码。好处很直接：问题在 review 阶段发现成本低，代码写完之后再发现成本高。每个 spec 的粒度要小，只做一件事。出错了就精准回溯：需求理解有偏差就回到 proposal 阶段重来，方向没问题只是代码写错了就定点修复。

两个阶段的分工：Vibe 负责方向，Spec 负责执行。这是 Formal Method 在实际开发中最自然的嵌入点。

---

三层结合模型：从需求到可验证代码

在两阶段工作流的基础上，Formal Method 可以进一步细化为三层结构，每一层都有具体的落地动作。

第一层：把需求写成 Semi-Formal 规约

这是整个体系的地基。不需要写 TLA+ 那种完整的数学证明，但要把需求里隐含的逻辑显式化。

核心方法是"自动形式化"（Autoformalization）：用 LLM 生成遵循预定义模板的规约，验证是轻量级的，依赖语法检查和编译成功。这些规约还可以作为"软约束"提供给 LLM 来引导后续的代码生成。

实操模板很简单，每个功能点写三项——前置条件、后置条件、不变量。以"用户下单"为例：

功能：用户下单

前置条件（Pre-condition）：
- 用户已登录
- 商品库存 > 0
- 订单金额 > 0

后置条件（Post-condition）：
- 库存减少对应数量（原子操作）
- 生成唯一订单号
- 支付状态初始为 PENDING

不变量（Invariant）：
- 任何时刻 库存 >= 0
- 订单号全局唯一
- 同一用户同一商品不能有两个 PENDING 状态的订单

把这个模板喂给 AI，它生成的代码质量会有质的提升——因为边界条件被显式声明了，AI 不需要猜。你确定"做什么"和"功能边界"，AI 负责"如何落地"和"实现细节"。

第二层：让 AI 对着规约生成代码

这是关键的 prompt 工程改变。对比一下两种写法：

普通 Vibe Coding 的 prompt 长这样：

“写一个下单接口，要处理库存”

加入 Formal 约束后的 prompt 变成这样：

"实现下单接口，必须满足以下规约：

• Pre: stock > 0 AND user.authenticated == true
• Post: stock’ = stock - quantity（原子）AND order.status = PENDING
• Invariant: stock >= 0 永远成立
• 边界场景：并发下单、库存恰好为1时的处理

用 Java Spring Boot 实现，包含完整的异常处理"

区别一目了然。前者给 AI 留了巨大的猜测空间，后者用精确的约束封住了最容易出错的地方。规约用领域导向的通用语言编写，混合自然语言与结构化元素（如 Given/When/Then 场景），充当"唯一真相来源"，让设计、实现、测试、文档都对齐到同一份契约。

第三层：可验证性检查

代码生成之后，需要三道防线来确保它真的符合规约。

属性测试（Property-Based Testing） 不是测"给定输入 A 得到输出 B"，而是测"对所有合法输入，某个属性始终成立"。Java 用 jqwik，Python 用 Hypothesis。

// 普通单元测试：测一个点
@Test
void testOrder() {
    assertEquals(PENDING, createOrder(user, item, 1).getStatus());
}

// 属性测试：测所有合法输入
@Property
void stockNeverNegative(
    @ForAll @IntRange(min=1, max=100) int initialStock,
    @ForAll @IntRange(min=1, max=5) int quantity
) {
    assume(quantity <= initialStock);
    Order order = orderService.create(user, item, quantity);
    assertThat(inventoryService.getStock(item))
        .isGreaterThanOrEqualTo(0);
}

属性测试对应 Formal Method 里的模型检验思想：枚举所有可能状态，验证不变量。普通单元测试是"我想到了这个 case 所以测一下"，属性测试是"对所有合法输入空间做系统性验证"。

断言驱动的防御性编程 把规约的 Pre/Post/Invariant 直接写成可执行的断言：

public Order createOrder(User user, Item item, int quantity) {
    // Pre-condition 检查
    assert user.isAuthenticated() : "用户未登录";
    assert item.getStock() > 0 : "库存为零";
    assert quantity > 0 : "数量非法";

    int stockBefore = item.getStock();

    // 核心逻辑
    Order order = doCreateOrder(user, item, quantity);

    // Post-condition 检查
    assert order.getStatus() == OrderStatus.PENDING;
    assert item.getStock() == stockBefore - quantity : "库存扣减错误";

    // Invariant 检查
    assert item.getStock() >= 0 : "库存不能为负";

    return order;
}

生产环境可以关闭断言，开发和测试环境打开——这些断言就是活的规约文档。

类型系统强化 用类型系统把不可能的状态变成编译错误。Discriminated Union 的目标是形式化基于字符串的状态/类型区分，防止语义漂移：

// 不好的写法：状态是字符串，任何地方都能写错
String status = "PEDING"; // 拼错了，运行时才发现

// Formal Method 思路：用枚举 + sealed class 让非法状态无法表示
public sealed interface OrderState
    permits Pending, Paid, Cancelled, Shipped {}

// switch 必须穷举所有状态，编译器帮你检查
Order order = switch(state) {
    case Pending p -> handlePending(p);
    case Paid p -> handlePaid(p);
    // 忘写 Cancelled 或 Shipped，编译报错
};

三种方式各有侧重：属性测试验证运行时行为，断言保护关键路径，类型系统在编译期拦截非法状态。组合使用，覆盖面远超传统单元测试。

---

企业落地：质量关卡不能省

数据告诉我们两件事。好消息是：Adidas 在 2024-2025 年的两次试点中，70% 的开发者报告生产力提升了 20-30%；某金融上市公司采用 AI Coding Agent 后研发效率提升近 40%，AI 生成代码可用率达 88% 以上。坏消息是：GitLab 2025 年的分析显示代码重复量增加了约四倍，代码 churn（过早合并后很快被重写）几乎翻了一番，代码重构量从 2021 年的 25% 降到了不足 10%——这意味着技术债在隐性积累。

这两组数据并不矛盾。AI 确实能大幅提升产出速度，但如果跳过 review 和测试，速度带来的就不是效率而是债务。

把三层模型整合成企业可执行的工作流，关键流程是这样的：业务需求进来后，先让 AI 帮你提取 Pre/Post/Invariant，人工 review 补充遗漏的边界；然后把规约文档作为 context 喂给 Coding Agent，AI 对着规约生成代码，同时要求它生成属性测试；代码生成后，运行属性测试自动枚举边界，检查断言覆盖率；最后 Code Review 只需重点看三件事——并发安全性、外部依赖的异常处理、规约里没覆盖到的隐性业务规则。

核心原则是：前置清晰度能产出显著更好的结果，而非一次性 prompting。

---

哪些场景最值钱

对于做企业级 Java 开发的团队，有三个场景最能体现这套体系的价值。

状态机业务（订单、审批流、工单）：用 Formal Method 把状态转移图写清楚，AI 生成的状态机代码就不会出现非法状态转移。sealed interface 配合穷举 switch，编译器替你兜底。

并发场景（库存、余额、计数器）：Pre/Post/Invariant 里显式声明原子性要求，逼着 AI 生成带锁或乐观锁的正确代码，而不是凭运气。属性测试可以用随机并发调度来暴露竞态条件。

接口契约（微服务边界）：每个接口的输入输出约束写进规约，自动生成的代码就有了可测试的合同，联调时问题定位速度翻倍。规约即文档，不会过期。

---

写在最后

Vibe Coding 的速度是真实的，Formal Method 的严谨也是真实的。把它们放在对立面上讨论没有意义——真正有意义的是找到正确的组合方式。

这套体系的本质可以用一句话概括：用 AI 想清楚需求，用规约约束 AI 写代码，用自动化验证把守质量关。 纯粹的"氛围感编程"适合玩具项目和快速原型，加上 Formal Method 的结构，才能走进企业的生产环境。

前置清晰度，而非事后修补。这才是 AI 时代软件工程的核心竞争力。