Alive2

alive2-mcp

Alive2 を使って LLVM IR の変換をチェックする MCP サーバーと CLI です。エージェントが最適化の正しさを証明または反証したり、パッチを適用した opt を trunk と比較したり、LLVM の Issue や PR で使われる alive2.llvm.org/ce/z/... リンクを読み取ったり作成したりできます。

デフォルトでは公開インスタンスの alive2.llvm.org に接続し、ローカルに alive-tv がある場合はそちらに接続します。ランタイム依存関係のない単一の静的 Go バイナリです。

ツール

ツール	機能	アノテーション
verify	関数ごとに、tgt が src を細分化しているかをチェックします。tgt は直接指定するか、passes からお使いの opt または trunk LLVM（opt: "upstream"）で生成します。各判定と、正しくない場合は Alive2 の反例を返します。	読み取り専用
create_link	チェック結果を短縮リンクとして公開し、送信した IR と一致することを確認するために読み戻します。	追加、冪等
get_link	短縮リンクから IR とオプションを読み取り、任意で再実行します。	読み取り専用

判定結果は correct、incorrect、unknown（タイムアウトまたは近似）および error です。 入力にはテキスト形式の IR（src、tgt）またはパス（src_file、tgt_file）を指定できるため、エージェントが大きなモジュールを貼り付ける必要はありません。結果は構造化コンテンツとして返されます。

インストール

方法	実行コマンド
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。通常はパッチを適用したビルドを指定します。指定しない場合、パスは 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		stdio の代わりにステートレスなストリーミング可能 HTTP を提供します。

CLI

同じバイナリをシェルから実行できます。終了ステータスは、正しい場合は 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 という名前の関数のみです。2 つのモジュールを指定した場合、両方に存在する関数をそれぞれ 1 つのモジュールに統合して名前を変更し、並行してチェックします。ターゲットの属性グループとメタデータは、ソース側と衝突しないように番号を振り直します。ローカルの alive-tv は両方のファイルを受け取り、関数の対応付けを自ら行います。

接続の切断、DNS タイムアウト、ゲートウェイエラーは、短いバックオフを挟んで 2 回再試行します。それ以外の 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 が取り込みます）とともにリリースを公開し、MCP Registry にバージョンを登録します。CI では、プッシュのたびに同じビルドをドライランとして実行します。

ライセンス

MIT。詳細は LICENSE を参照してください。