Alive2

alive2-mcp

一个用于检查 LLVM IR 转换的 MCP 服务和命令行工具，基于 Alive2。它可以让 Agent 证明或反驳某项优化是否正确、将修补版 opt 与 trunk 进行比较，并读取或创建 LLVM 问题和 PR 中使用的 alive2.llvm.org/ce/z/... 链接。

默认连接到公共实例 alive2.llvm.org，如果你有本地 alive-tv，也可以连接到它。它是一个独立的静态 Go 二进制文件，无需运行时依赖。

工具

工具	功能	注释
verify	按函数检查 tgt 是否细化了 src。tgt 可以直接提供，也可以由你的 opt 根据 passes 生成，或由 trunk LLVM 生成（opt: "upstream"）。返回每项判定；如果结果不正确，还会返回 Alive2 的反例。	只读
create_link	将检查发布为短链接，然后读取该链接以确认其内容与提交的 IR 一致。	追加式、幂等
get_link	将短链接读回为 IR 和选项，并可选择重新运行检查。	只读

判定结果为 correct、incorrect、unknown（超时或近似结果）和 error。 输入可以是 IR 文本（src、tgt），也可以是文件路径（src_file、tgt_file），因此 Agent 无需粘贴大型模块。结果以结构化内容返回。

安装

方式	命令
Homebrew（macOS、Linux）	brew install phongndo/tap/alive2-mcp
mise	mise use -g github:phongndo/alive2-mcp
Go	go install github.com/phongndo/alive2-mcp@latest
Nix	nix profile add github:phongndo/alive2-mcp
Docker	docker pull ghcr.io/phongndo/alive2-mcp
下载	Linux、macOS 和 Windows 的归档文件可在发布页面获取

它也已列入 MCP Registry，名称为 io.github.phongndo/alive2-mcp。发布归档包含构建来源证明；可使用 gh attestation verify <archive> --repo phongndo/alive2-mcp 验证。

使用

Claude Code

claude mcp add alive2 -- alive2-mcp -opt /path/to/build/bin/opt

或在项目的 .mcp.json 中配置：

{
  "mcpServers": {
    "alive2": { "command": "alive2-mcp", "args": ["-opt", "build/bin/opt"] }
  }
}

Codex

codex mcp add alive2 -- alive2-mcp -opt /path/to/build/bin/opt

无需安装

该镜像通过 stdio 运行服务。它无法访问你的文件或 opt，因此请将 IR 作为文本传入，并使用 opt: "upstream"：

{
  "mcpServers": {
    "alive2": { "command": "docker", "args": ["run", "-i", "--rm", "ghcr.io/phongndo/alive2-mcp"] }
  }
}

标志

标志	环境变量	含义
-opt PATH	ALIVE2_MCP_OPT	用于将 passes 转换为 tgt 的默认 opt，通常是你的修补版构建。未设置时，passes 将由 upstream 运行。
-alive-tv PATH	ALIVE2_MCP_ALIVE_TV	本地 alive-tv；检查将在本地运行，不使用网络。
-web URL	ALIVE2_MCP_WEB	Alive2 Compiler Explorer 实例（默认值：https://alive2.llvm.org/ce）。
-http ADDR		使用无状态、可流式传输的 HTTP 服务，而不是 stdio。

命令行工具

同一个二进制文件也可以在 shell 中使用。正确时退出状态为 0，其他情况为 1，错误时为 2，因此适用于脚本和 git bisect run。

alive2-mcp -opt build/bin/opt verify -passes gvn repro.ll   # your patch
alive2-mcp verify -opt upstream -passes gvn repro.ll        # trunk LLVM
alive2-mcp verify before.ll after.ll                        # two files, matched by name
alive2-mcp get-link -verify https://alive2.llvm.org/ce/z/_kCuTV
alive2-mcp link -function f before.ll after.ll              # publishes

工作原理

Alive2 网站是一个运行 alive-tv 编译器的 Compiler Explorer 实例，因此本工具使用 Compiler Explorer 的 API： /api/compiler/alive/compile、/shortener 和 /api/shortlinkinfo/<id>。

该网站只会比较名为 @src 和 @tgt 的函数。对于两个模块，它会将双方共有的每个函数合并到一个模块中，重命名后并发检查。目标模块的属性组和元数据会重新编号，以避免与源模块冲突。本地 alive-tv 会获取两个文件并自行配对函数。

连接中断、DNS 超时和网关错误会在短暂退避后重试两次。其他 HTTP 错误会立即报告。

限制

Alive2 的分析有界，且仅限过程内。循环只展开几次，对其他函数的调用视为不透明，因此 correct 是有力证据，而非证明。发送到网站的任何内容都会发送到公共服务，而 create_link 会永久保存内容。

开发

nix develop          # Go, gopls, golangci-lint, nixfmt
go test -race ./...  # unit tests against a fake Alive2 server
nix flake check      # build, tests, golangci-lint, formatting

CI 会在 Linux（x86-64 和 ARM）和 macOS 上运行 nix flake check。每周还会检查 alive2.llvm.org API 的实时状态，因为该 API 的变更会导致此工具无法正常工作。

要发布，请设置 VERSION，并在 main 上推送匹配的 vX.Y.Z 标签。Release 工作流会使用 GoReleaser 构建归档文件和 镜像，为其生成证明，发布包含 Homebrew formula 的版本 （phongndo/homebrew-tap 会获取该 formula），并将该版本列入 MCP Registry。每次推送时，CI 都会以试运行的方式执行相同的构建。

许可证

MIT；详见 LICENSE。