AI 编码 Agent 写完代码就放心了？Forall 用形式化验证确保每行代码都经得起推敲

如果你正在用 Claude Code、Cursor 或 Codex 编写重要代码，你可能已经经历过这个场景：Agent 飞快地生成了一大段代码，测试通过，功能看起来也正常——但你心里总有个声音在问：”它真的对吗？边缘情况都覆盖了吗？”

这不是杞人忧天。AI 编码 Agent 生成的代码在常规路径上通常表现良好，但在边界条件、并发竞态、类型契约违背等场景中，往往藏着不易察觉的 Bug。传统的单元测试只能验证你想到的情况，而”没想到的情况”才是真正的风险源。

痛点：直觉验证 vs 形式化验证

Forall（∀） 来自 Astrio 团队（160⭐, Apache-2.0），它的核心思路很简单但意义深远：让 AI 编码 Agent 在声称”Done”之前，必须先生成可机器验证的证明（proofs）。这不是增加负担，而是把验证从”人工靠经验”升级为”机器靠逻辑”。

两种使用方式

Forall 提供两种集成路径，适应不同的工作流：

路径 A：Forall CLI（完整编码 Agent）

如果你是追求端到端规范驱动开发的开发者，可以直接把 Forall 作为主力编码 Agent：

curl -fsSL https://forall.astrio.app/install.sh | bash
forall

首次启动时，你可以选择使用 Forall 账号（浏览器打开 dashboard 创建 API Key）或自带模型 API Key（OpenAI / OpenRouter）。然后在 Git 仓库根目录初始化项目：

forall init
forall

Forall 的 CLI 是一个全功能的终端 UI 编码 Agent，内置工作流管理、形式化验证和代码生成能力。

路径 B：MCP 验证桥接（保留现有 Agent）

如果你已经习惯使用 Claude Code、Cursor 或 Codex，不想切换工具，Forall 的 MCP 验证桥接方案是更轻量的选择：

{
  "mcpServers": {
    "forall": {
      "command": "npx",
      "args": ["-y", "@astrio/forall-mcp"],
      "env": {
        "FORALL_API_KEY": "forall_..."
      }
    }
  }
}

这个方案不会读写你的工作区——它只提供验证服务。你的编码 Agent 从验证报告中获取问题反馈，然后自行修复代码。API Key 在 forall.astrio.app/dashboard 免费创建。

规范驱动的工作流

Forall 倡导一种五步走的工作流：

propose → specs → apply → verify → archive

Propose：启动一个命名的变更。Forall 会在 .forall/workflow/changes// 下创建提案目录。

forall propose add-search-filter

Write specs：在写代码之前，先描述你期望的行为。Specs 保存在变更目录中，作为需求文档。

Apply：实现变更。Forall 在后台同步维护需求与代码的映射关系。

Verify：运行检查确认变更满足需求：

forall check --change add-search-filter

Archive：检查通过后归档变更，记录结果：

forall archive add-search-filter

这个工作流的精妙之处在于：Specs 在前，代码在后。先明确”做什么”，再让 Agent 去”怎么做”。这与传统 AI Agent “你说需求我直接写代码”的模式形成鲜明对比——前者是可验证、可追溯的工程流程，后者是黑盒输出。

项目结构

forall init 会在项目根目录创建 .forall/ 目录，结构如下：

.forall/
├── markers.toml           # 标记项目根
├── workflow/
│   ├── config.yaml        # 工作流 Schema 和项目规则
│   ├── changes/           # 进行中的变更
│   └── archive/           # 已完成的变更
└── verify/
    └── mapping.yaml       # 需求 → 代码映射

这份 workflow/config.yaml 配置文件是可提交到 Git 的——整个团队共享相同的 Specs 和验证规则：

schema: forall
context: |
  This project uses the Forall workflow. Write specs before code.
  Run `forall check` before archive.
rules:
  verification:
    - Run `forall check --change ` and fix all CRITICAL issues before archive

支持的编程语言

目前 Forall 支持三种语言的形式化验证：

团队表示正在根据社区需求扩展到更多语言。

MCP 验证工具的细节

如果你使用路径 B（MCP 桥接），Forall 提供 4 个核心 MCP 工具：

通过 MCP Streamable HTTP 协议（https://mcp.forall.astrio.app/mcp）通信，验证在隔离的 Worker 中异步执行。支持两种输入方式：

// 内联文件
{
  "source": {
    "type": "inline",
    "files": [{ "path": "src/lib.rs", "content": "..." }]
  },
  "scope": { "type": "project" },
  "strict": false
}

// 公共 GitHub 仓库
{
  "source": {
    "type": "github",
    "repository": "owner/repository",
    "ref": "main"
  }
}

横向对比：Forall vs 传统代码质量方案

注意事项

• Forall CLI 的二进制核心是闭源的（通过 install.sh 下载的预编译包），但项目的 SDK、MCP 桥接层和文档仓库采用 Apache-2.0 开源
• 路径 A 和路径 B 互斥：使用 Forall CLI 时不要手动添加 MCP URL，反之亦然
• 支持平台：macOS（Apple Silicon + Intel）、Linux（x86_64 + aarch64）、Windows（x86_64）
• API Key 免费创建：在 forall.astrio.app/dashboard 注册即可获得
• 不支持私有 GitHub 仓库验证（截至当前版本），如果需求强烈，关注他们的 Discord 更新

总结

Forall 不是又一个 AI 编码 Agent——它是一种验证范式的升级。它把”写代码→测试→祈祷”的旧模式，变成了”写 Specs→实现→机器证明”的新模式。对于构建关键业务逻辑、安全敏感模块、或需要长期维护的代码库来说，这种”Specs 优先”的思路，可能正是 AI 编码时代最需要的那层保险。

相关链接：

• GitHub 仓库
• Forall 官网
• MCP 验证包（npm）
• Discord 社区