让 AI 生成的账本逻辑通过证明再上 JVM

AI 写出转账代码，再补上一批通过的单元测试，离「资金不会凭空增减」还有多远？这篇文章给出的路线是：让 AI 用 Lean 4 编写业务函数和不变量证明，构建时检查证明，再把代码放进 Clojure 服务运行。

连接这两端的是 Ansatz Lean/JVM SDK。它把 Lean 代码打包成 .leanjvm，交给 JVM 上的解释器执行。值得读的地方，是证明、部署和宿主调用终于串成了一条流程；需要追问的地方，则是证明到底覆盖了哪些业务行为。

证明能拦住测试容易漏掉的什么错误

作者选择了一个很小的账本模型：发送方、接收方和转账金额都用自然数 Nat 表示，余额下限设为零，转账前后双方余额总和必须相等。

漏洞出在减法。

Lean 的 Nat 不包含负数，3 - 5 = 0。如果直接计算发送方余额减去金额，同时给接收方加上金额，余额不足时就会凭空多出资金。发送方只有 3，却转出 5，结果是发送方归零、接收方增加 5。

单元测试可以发现这个例子，但前提是测试写到了它。形式化验证（formal verification）要求证明一个命题：对于函数接受的所有输入，余额总和都保持不变。

作者展示的第一次证明无法完成，编译器留下未解决目标。随后，代理增加余额检查，余额不足时返回原余额：

namespace Ledger

def settleTransfer (fromBal toBal amount : Nat) : (Nat × Nat) :=
  if amount ≤ fromBal then
    (fromBal - amount, toBal + amount)
  else
    (fromBal, toBal) -- Rejected transfer preserves balances unchanged

/-- Theorem: Transfers strictly conserve total capital. -/
theorem settle_conserves_value (fromBal toBal amount : Nat) :
  let (f, t) := settleTransfer fromBal toBal amount
  f + t = fromBal + toBal := by
  unfold settleTransfer
  split
  · rename_i h
    omega
  · rfl

/-- Theorem: The sender account never drops below zero (solvency guarantee). -/
theorem settle_preserves_solvency (fromBal toBal amount : Nat) :
  let (f, _) := settleTransfer fromBal toBal amount
  f ≤ fromBal := by
  unfold settleTransfer
  split
  · rename_i h
    omega
  · rfl

end Ledger

关键是 if amount ≤ fromBal：它让扣款只在余额充足时发生，证明也随之分成成功和拒绝两个分支。

这里要读准第二个定理。f ≤ fromBal 证明的是发送方余额不会增加；余额不小于零，则来自 Nat 的取值范围。它没有覆盖可配置的负数透支下限。

证明覆盖的是写出来的命题，以及命题采用的数据模型。

原文称两项证明通过，但没有提供完整项目、编译日志或代理交互记录。可以把它当成流程演示，不能据此判断代理在复杂账本上的成功率。另外，未解决的证明目标也不等于具体反例，编译器报错还需要代理继续分析。

Lean 的证明，怎样进入普通 JVM 服务

原文使用的依赖是 org.replikativ/ansatz-lean-jvm:0.2.615，架构图标注的工具链是 Lean 4.33.1。它把工作分成两个阶段。

构建时，原生 Lean 工具链检查代码与证明，擦除证明，再把中间表示（IR）、类型和布局打包成 .leanjvm。文中给出的构建环境是带 prlimit 的 Linux x86-64，或者 Docker。

下面的命令负责准备可部署产物：

java -cp "$SDK_CLASSPATH" ansatz.lean.jvm.LeanPreparation \
  --source ./ledger \
  --sysroot "$LEAN_SYSROOT" \
  --producer-bundle "$PRODUCER_BUNDLE" \
  --cache "$COMPILER_CACHE" \
  --root-module Ledger \
  --entry Ledger.settleTransfer \
  --output ./ledger.leanjvm

要留意 --entry Ledger.settleTransfer，它指定了入口函数；--sysroot、--producer-bundle 和 --cache 对应的资源如何准备，原文没有展开。命令生成 ledger.leanjvm，并输出 SHA-256 指纹，文中展示的是缩写 sha256:d8a2...3f10，不能直接拿来做校验配置。

运行时，生产容器只需标准 OpenJDK 17+ 和 SDK，由纯 Java 解释器加载产物，不再安装 Lean 工具链，也不需要原生 C 或 JNI 桥接。运行状态由 JVM 垃圾回收器管理。

Clojure 侧通过 lean/open 创建运行时，用 lean/load-artifact 加载产物，并传入环境变量 EXPECTED_MANIFEST_SHA256。再用 lean/function 获取 Ledger.settleTransfer。

文中的调用结果很直观：10000 1000 500 返回 [9500N 1500N]；超额转账 10000 1000 15000 返回 [10000N 1000N]。返回值是 Clojure 持久向量，其中数字是 java.math.BigInteger。

部署依赖确实少了一层，但执行方式仍然是解释 IR。原文没有给出吞吐、延迟、内存占用，也没有与原生 Lean 或直接用 Clojure 实现进行比较。架构图还提到默认 2M ops 指令预算，却没有展示配置入口或预算耗尽时的处理方式。

接上手续费和外部 IO，原来的保证还成立吗

真实业务要查数据库或配置。SDK 允许 Lean 声明外部函数，再由 Clojure 提供实现。

示例通过 @[extern "ansatz_jvm_account_fee"] 声明 getAccountFee : String → IO Nat，在宿主绑定中使用 Ledger.getAccountFee，并指定 :implementation-id "fees/v1"、:effect :io 和 :fn。

费率按千分比计算：vip 返回 0N，standard 返回 15N，对应 1.5%；默认返回 50N，对应 5.0%。settleWithFee 计算 (amount * feeRate) / 1000，检查转账金额与手续费之和是否超过余额。

Clojure 用 lean/call 调用 IO 函数，拿到 IOResult 后，通过 .isOk、.getValue 和 .getError 处理结果。文中转出 2000、手续费 30，最终得到 [7970N 3000N]。

但这段代码没有附带证明。更直接的问题是，两个账户原来合计 11000，现在合计 10970。少掉的 30 没有进入示例中的手续费账户，所以前面的双账户守恒定理不能直接套用。

这不一定是业务错误，却要求重新定义守恒范围：手续费归谁，是否需要加入第三个账户，哪些输入和返回值受到约束。

作者认为，对宿主输入进行参数化的证明可以继续成立。这个判断有条件：函数行为和宿主返回值必须满足证明中的假设。数据库查询、重复请求、写入原子性，并不会因为接入 Lean 就自动得到验证。

原文另一个卖点是执行状态分叉：引擎内部可以复制调用帧、堆对象和寄存器，让计算从暂停点走向不同分支。但公共 SDK 尚未暴露 fork handles，当前不能把它当作可直接使用的接口。

丢弃计算分支，也不能据此推断数据库写入会撤销。原文所谓无需数据库回滚的设想，需要外部副作用尚未提交，或另有隔离机制。

我的判断

我认可这条路线最具体的价值：AI 修改实现后，必须重新通过明确的不变量检查。对于边界清楚的计算规则，这比继续要求模型「多考虑一些边界情况」更容易形成约束。

不过，文章没有证明整套金融服务正确，也没有给出代理效率、运行性能或维护成本的对照数据。关于它是否更适合一般团队，目前仍是方案展示和经验判断。

与常见的单元测试、属性测试相比，Lean 能对明确命题给出更强的保证，代价是团队要维护规格、证明和工具链。前两者仍适合检查接口、序列化、持久化等集成行为。

最值得先投入的，是失效代价高、规则稳定、输入输出边界清楚的那部分逻辑。

还要避免另一种误用：模型把规格写弱了，证明照样可能通过。人需要审查「究竟证明了什么」，不能只看构建是否变绿。

能拿来做什么

• 给 AI 编写计算逻辑时，先列出可检查的不变量。例如这篇转账模型中的余额总和不变、余额不足时双方余额不变，再决定采用测试、属性测试还是形式化证明。
• 已有 Clojure 或 Java 服务的团队，可以选一个独立纯函数试接 .leanjvm，同时验证构建环境、产物指纹、默认指令预算和实际调用成本。
• 为手续费等规则增加外部输入时，先更新业务模型和守恒范围，再补证明。宿主回调能返回什么、失败如何处理，都应成为接口约定。
• 前端或 Node 团队可以借鉴「生成、检查、修正」的反馈流程；原文展示的 SDK 面向 JVM，没有给出浏览器或 Node 的直接运行方案。