Forall 实战：把 AI 编码的规格、变更与异步验证拆成两条可检查的路径
让 AI 编码 Agent 一次改完需求，最难的往往不是生成代码，而是回答三个后续问题：这次改动究竟承诺了什么？实现有没有偏离承诺？检查结果该由谁处理？如果这些信息只留在一次对话的上下文里，下一位开发者或下一轮 Agent 很难复核。
Forall 提供了一种值得拆开的思路：把项目内的规格与变更工作流，以及可由外部 Agent 调用的托管验证，明确分成两条路径。它的目标不是替开发者宣称“所有代码都已被形式化证明正确”，而是让需求、实现映射、验证任务和报告成为可保存、可检查的工程对象。当前公开文档列出的面向应用代码的支持语言是 TypeScript、Java 与 Rust；仓库自身则主要以 Rust 实现。
这类设计属于“编程语言、框架、开发者工具、测试与软件架构”范畴：它讨论的重点不是替换编辑器，而是把 AI 参与的改动纳入可审计的变更流程。
先分清两条路径：完整 Agent 与 verify-only MCP
Forall 的架构文档刻意避免把所有能力塞进一个 MCP Server。第一条路径是官方 forall CLI：它提供终端界面、工作流命令、原生工具和沙箱，直接面对本地工作区。第二条路径是给 Cursor、Claude Code、Codex 等宿主 Agent 使用的 MCP bridge：它只提交并查询验证，不会替外部 Agent 写入用户工作区。
这一区分很重要。外部 Agent 负责理解仓库、提出或执行修改；Forall 的托管验证服务返回报告；修复动作仍由宿主 Agent 或人来决定。于是验证器不必拥有任意写文件权限，调用方也不能把“报告已返回”误当成“代码已经修好”。
还要准确看待开源边界：仓库与公开组件采用 Apache-2.0，但官方架构文档说明，完整 CLI Agent runtime 以预构建的 forall 二进制交付，公开仓库不包含 TUI、Agent turn loop、sandbox 和原生工具注册表的完整源码。因此适合把它当作“公开工作流/验证组件加官方二进制”的组合，而不是笼统说成所有运行时都开源。
在仓库中保存“这次改动是什么”
在已有 Git 项目的根目录，官方给出的最小启动方式如下：
curl -fsSL https://forall.astrio.app/install.sh | bash forall --version cd your-repository forall init forall
forall init 会建立 .forall/ 目录。公开的项目布局文档列出三个关键文件：.forall/markers.toml 用来标记项目根；.forall/workflow/config.yaml 保存工作流 schema、上下文与规则；.forall/verify/mapping.yaml 保存需求到实现代码的映射。官方建议把 .forall/ 作为项目共享配置提交到版本控制，而把机器本地状态留在 ~/.forall/，不要混入仓库。
这种安排把“为什么要改、哪些文件实现了它、怎样验证”从聊天记录里移到了代码评审能看到的位置。它不自动消除规格本身的歧义，却能让歧义更早暴露：如果需求无法映射到可检查的实现，团队至少不会在合并之后才发现没有可验证的落点。
用 propose → check → archive 管理一次变更
Forall 文档给出的工作流不是一个模糊的“让 Agent 自己做完”，而是一组显式阶段：propose → (specs / design) → apply → verify → archive。可从下面的骨架开始：
forall propose add-rate-limit forall check --change add-rate-limit forall archive add-rate-limit
这里最有价值的不是命令数量，而是归档前的门槛。把 check 放在归档之前，意味着“代码可运行”之外还要检查变更是否满足已写下的工作流约束。实际团队仍应把单元测试、集成测试、人工代码评审与部署前检查保留在 CI 中；Forall 的流程是补充规格和证据链，不是取代现有质量门禁。
让既有 Agent 使用托管验证，但别扩大权限
若团队已经使用其他编码 Agent，不一定要切换到完整 Forall CLI。官方的 @astrio/forall-mcp 是一个 stdio MCP bridge，它把本地客户端连接转发到托管 MCP 服务。文档给出的配置结构如下；API Key 应放入本地安全配置或密钥管理系统，不能提交进仓库：
{
"mcpServers": {
"forall": {
"command": "npx",
"args": ["-y", "@astrio/forall-mcp"],
"env": {
"FORALL_API_KEY": "forall_..."
}
}
}
}
这条 verify-only 路径提供 forall_verify、forall_verification_status、forall_cancel_verification 和 forall_explain_verification 等工具。验证以异步 job 运行：提交后会经历 queued、preparing、running，最终到 succeeded、failed、cancelled 或 expired 等状态。外部 Agent 可以提交内联文件内容，也可以提交公共 GitHub 仓库与 ref；私有仓库 OAuth 和远程 authoring 在文档中仍标为 deferred，不能把它们写成现成功能。
异步设计的实际好处是把慢检查从一次对话回合中拆出：调用方可以先取得 job ID，再轮询状态和经清理的报告。代价是工程上必须处理超时、失败、取消和报告过期，而不是只在提示词里要求 Agent “验证一下”。托管服务文档还说明报告会清理容器路径、环境变量、凭据和原始命令行；这不等于无需保密，向服务提交源码或文件内容前仍应按组织的数据边界评估。
把验证结果接回工程流程，而不是接回聊天记录
一个更稳妥的接入方式，是把验证 job 当作 CI 中一个有状态的外部检查：提交请求后记录 job ID；在规定的等待窗口内查询状态；成功时把报告摘要贴到代码评审或变更记录；失败、取消或过期时明确标为“未获得验证结果”，而不是把它折算成通过。Forall 文档已经把这些终态区分开，调用方也应保留这种区分。否则，网络错误、服务端失败和真正的验证成功会在自动化链路里被混成同一个布尔值。
对于会反复修改同一需求的 Agent，报告还应被视为下一轮输入，而不是一次性的装饰文本。例如，先让宿主 Agent 根据 forall_verification_status 的发现项缩小修改范围，再重新提交验证；没有必要因为一个报告就要求它重写整个模块。这样做能把“发现—修复—复验”限制在同一变更目录和同一规格边界内，也使审阅者能够追溯：哪一次实现对应哪一份检查结果。
权限边界同样需要落实到配置层。verify-only MCP 的价值在于验证服务不直接写工作区，但宿主 Agent 仍可能拥有 shell、Git 或部署权限。团队不能仅因增加了一个只读验证器，就放宽其他工具的执行权限。更合理的做法是继续按现有规则隔离测试凭据、生产凭据和发布动作，并在变更归档前由人确认高风险修改。Forall 提供的是更清晰的证据接口，不是取代权限设计的安全产品。
适用场景与落地边界
Forall 特别适合两类场景：一类是多人或多 Agent 持续修改同一代码库，需要把规格和变更历史留在 Git 中；另一类是已有 Claude Code、Codex 或 Cursor 工作流，但希望把验证职责作为独立、低权限的 MCP 能力接入。对于一次性脚本、小型原型，维护 .forall/ 配置和变更档案的成本未必划算。
它也不适合被当成“先让 Agent 任意改、最后再补一份证明”的工具。若需求没有稳定的验收边界、接口仍在频繁推翻，过早建立过细的映射可能只会制造维护负担。此时应先把产品决策、兼容性策略和测试基线稳定下来，再把真正需要长期追踪的约束写进变更流程。相反，对于鉴权、计费、数据迁移、限流或跨服务契约等高影响改动，能把规格、实现位置和复验结果关联起来，通常比单纯增加一次模型审查更有价值。
落地时建议先挑一个边界清晰的需求试运行，例如新增限流规则或一个 API 字段：先写可审查的规格，再用 forall propose 建立变更，保留既有测试，最后把 check 报告作为评审输入。试运行结束后，可由团队复盘三个问题：规格是否帮助缩小了修改范围、报告是否真的影响了评审决定、归档记录能否让不了解原始对话的人复现判断。只有这些答案为“是”，再扩大到更多仓库和更多 Agent 才有意义。真正要避免的是把“规格驱动”变成多写几份没人读的文档。规格、实现映射、测试和归档只有在同一条交付路径上被持续使用，才会成为 AI 编码流程中的可靠约束。
相关链接