AI Agent 写错代码怎么办？LLMLL 用形式化契约把错误挡在合并之前
AI 编程 Agent 最大的风险，不是不会生成代码，而是能生成一段类型正确、测试暂时也能通过、但业务含义错误的代码。LLMLL（Large Language Model Logical Language）选择了另一条路线：让 Agent 填写带类型和契约的代码空洞，再由编译器和 SMT 求解器检查实现是否满足契约；验证失败时，补丁不会被接受。
这个项目来自 Hacker News 的低分新项目，仓库采用 GPL-3.0，并把自己定位为实验性的编程语言与验证流水线。它不声称“证明了整个程序正确”，而是明确保证：代码必须符合开发者写下的规格，且每个结果会区分 verified、asserted 和无法证明等状态。这个边界意识，反而是它最值得借鉴的地方。
它解决的不是普通单元测试问题
LLMLL 的核心对象是 hole。?hole 不是一个任意的 TODO，而是带有输入类型、前置条件、后置条件和当前作用域信息的待实现位置。Agent 通过 checkout 获取契约上下文，提交者再用 patch 写入实现。补丁需要重新类型检查，并通过 SMT 验证，才会写回程序。
以转账为例，契约不只是检查余额不能为负，还可以约束两个返回余额的总和保持不变：转账前后的总额必须守恒。一个“给收款方凭空加钱”的实现，即使语法和类型都正确，也会在验证阶段被拒绝。README 中的 conserve 示例正是用这个关系性质展示错误实现如何被 refuted。
这带来一种比“让 Agent 自己跑测试”更强的协作协议：主 Agent 负责定义类型和“应该满足什么”，专门的 Agent 负责填“如何实现”，编译器负责在合并点检查两者是否一致。
一条可复现的验证路径
项目官方提供 Docker 镜像，省去 Haskell、Z3 和 liquid-fixpoint 的本地安装。最小示例可以这样运行：
# 验证一个故意错误的支付实现 docker run --rm ghcr.io/machunter/llmll verify /opt/llmll/examples/payments-core/conserve-bad.llmll # 挂载自己的工作目录 docker run --rm -v "$PWD":/work ghcr.io/machunter/llmll verify myfile.llmll
从源码构建时，官方文档要求 GHC 至少 9.4、Stack 至少 2.9，证明路径还需要 Z3 和 liquid-fixpoint。常用命令包括：
llmll check program.llmll --strict llmll holes program.llmll --deps llmll verify program.llmll --weakness-check --spec-coverage
check 负责解析和类型检查；holes 列出未完成的实现，还能输出依赖图；verify 才是契约证明入口。缺少求解器时，项目会明确报告“没有证明”，并以退出码 3 结束，而不是把“没运行验证”伪装成成功。
目前的边界必须看清
LLMLL 当前的主证明路径是基于 Z3 和 liquid-fixpoint 的非递归 QF-LIA 核心，擅长整数线性算术、条件分支、契约函数调用以及组合式的调用链推理。非线性运算、部分递归和复杂字符串结构并不会自动变成已证明事实。
项目还提供实验性的 Leanstral 路径，用于某些非线性义务，但文档明确要求 Lean 4、Mathlib 和 API key，并把它标记为实验功能。换句话说，团队不能看到 verified 就宣称“系统绝对安全”；还应该检查契约是否足够强、哪些部分只是 asserted，以及哪些目标超出了求解器能力。
另一个有价值的检查是 --weakness-check：如果契约弱到一个无意义的函数体也能满足，工具会提示问题；--cdp 则用于评估契约排除错误实现的能力。它们把“规格写得好不好”也纳入工程反馈，而不是只盯着 Agent 生成了多少代码。
适合怎样接入 AI 编程流程
LLMLL 不必替代现有测试。更现实的做法是分层使用：先让 Agent 生成实现，再用常规测试覆盖样例和集成行为，最后对支付、权限、资源边界、协议状态机等关键函数写精确契约。只有这些关键函数进入 verified 状态，才允许自动合并；普通辅助逻辑可以保留测试或 asserted 标记。
如果要在多 Agent 团队中采用它，可以把 checkout → patch → verify 作为写入协议：每个 Agent 只能领取明确的 hole，提交的 JSON Patch 必须经过重新验证，调用链中的子函数也要有自己的契约。这样，代码评审的重点就从“这段生成代码看起来像不像对的”，转向“它满足了什么可检查的性质”。
LLMLL 仍是实验项目，语言、编译器和 Leanstral 集成都可能变化；但它提出了一个很务实的方向：不要要求 Agent 凭直觉保证正确，而是让 Agent 在可执行规格的边界内工作。对于任何准备把 AI 生成代码接入生产合并流程的团队，这种“先证明，再合并”的门槛值得提前设计。