Show HN: Forall – 生成机器可验证证明的 AI 编码代理

英文标题：🔶 Show HN: Forall – An AI coding agent that generates machine-checkable proofs

Forall 是来自 Astrio 的一个 AI 编码代理，它能够根据规范生成代码，并同时生成可被机器检查的形式化证明，从而提升软件正确性。开发者可以通过命令行工具安装使用，或通过 MCP 集成到现有编码代理（如 Cursor、Claude Code）中。该项目开源，支持多种语言，并欢迎社区参与。这种将形式化验证引入 AI 辅助编程的尝试，对追求高可靠性软件的开发者具有重要意义。

打开原文相关 6 · 机会 1

中文

Forall 是来自 Astrio 的一个编码代理，通过生成规范驱动的代码以及伴随的机器可检查证明，帮助开发者构建正确软件。

完整的编码代理 —— 在终端中处理规范、证明和工作流。

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

将 ~/.local/bin 添加到你的 PATH（如果需要），然后运行 forall --version。

首次启动时，使用 Forall 账户（API 密钥）登录，或者提供你自己的模型 API 密钥（OpenAI / OpenRouter）。然后在 git 仓库中运行 forall init 开始工作。

注意： 安装前必须存在一个二进制发布版本于 GitHub Releases。

继续使用 Cursor、Claude Code 或 Codex —— 通过 MCP 添加托管验证。不要安装 CLI。

在 forall.astrio.app/dashboard 创建 API 密钥。
添加到你的 MCP 客户端配置：

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

你的编码代理会根据验证报告编辑工作区。详细参见 docs/getting-started.md 和 docs/hosted-mcp.md。

支持的编程语言

我们正在根据需求扩展到更多语言。

加入我们的 Discord 和 X 社区。

本仓库根据 Apache-2.0 许可证授权。

English / 原文

Forall is a coding agent from Astrio that helps developers build correct software by generating spec-driven code alongside machine-checkable proofs.

Full coding agent — specs, proofs, and workflow in your terminal.

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

Add ~/.local/bin to your PATH if needed, then run forall --version.

On first launch, sign in with a Forall account (API key) or bring your own model API key (OpenAI / OpenRouter). Then forall init in a git repo and start working.

Note: A binary release must exist on GitHub Releases before install succeeds.

Stay on Cursor, Claude Code, or Codex — add hosted verification via MCP. Do not install the CLI.

Create an API key at forall.astrio.app/dashboard
Add to your MCP client:

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

Your coding agent edits the workspace from verify reports. See docs/getting-started.md and docs/hosted-mcp.md.

Supported programming languages

We are expanding to more languages based on demand.

Join our Discord and X communities.

This repository is licensed under the Apache-2.0 License.