Alive2

alive2-mcp

An MCP server and CLI for checking LLVM IR transformations with Alive2. It lets an agent prove or refute that an optimization is correct, check a patched opt against trunk, and read or create the alive2.llvm.org/ce/z/... links used in LLVM issues and PRs.

It talks to the public instance at alive2.llvm.org by default, and to a local alive-tv when you have one. It's a single static Go binary with no runtime dependencies.

Tools

Tool	Does	Annotations
verify	Checks that tgt refines src, per function. tgt is given directly, or produced from passes by your opt or by trunk LLVM (opt: "upstream"). Returns each verdict and, when not correct, Alive2's counterexample.	read-only
create_link	Publishes the check as a short link, then reads it back to confirm it holds the submitted IR.	additive, idempotent
get_link	Reads a short link back into IR and options, and optionally re-runs it.	read-only

Verdicts are correct, incorrect, unknown (timeout or approximation) and error. Inputs take IR as text (src, tgt) or as paths (src_file, tgt_file), so agents don't have to paste large modules. Results are returned as structured content.

Install

With	Run
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
Download	archives for Linux, macOS and Windows on the releases page

It's also listed in the MCP Registry as io.github.phongndo/alive2-mcp. Release archives carry build provenance; verify one with gh attestation verify <archive> --repo phongndo/alive2-mcp.

Use

Claude Code

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

or in a project's .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

Without installing

The image runs the server over stdio. It can't see your files or your opt, so pass IR as text and use opt: "upstream":

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

Flags

Flag	Env	Meaning
-opt PATH	ALIVE2_MCP_OPT	Default opt for turning passes into tgt, typically your patched build. Without it, passes run upstream.
-alive-tv PATH	ALIVE2_MCP_ALIVE_TV	Local alive-tv; checks then run locally, with no network.
-web URL	ALIVE2_MCP_WEB	Alive2 Compiler Explorer instance (default https://alive2.llvm.org/ce).
-http ADDR		Serve stateless streamable HTTP instead of stdio.

CLI

The same binary works from a shell. Exit status is 0 for correct, 1 for anything else and 2 for errors, so it fits scripts and 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

How it works

The Alive2 website is a Compiler Explorer instance running alive-tv as a compiler, so this uses Compiler Explorer's API: /api/compiler/alive/compile, /shortener and /api/shortlinkinfo/<id>.

The website only compares functions named @src and @tgt. For two modules, each function they share is merged into one module, renamed, and checked concurrently. The target's attribute groups and metadata are renumbered so they can't collide with the source's. A local alive-tv gets both files and pairs functions itself.

Dropped connections, DNS timeouts and gateway errors are retried twice with a short backoff. Other HTTP errors are reported at once.

Limits

Alive2 is bounded and intraprocedural. Loops are unrolled a few times and calls to other functions are opaque, so correct is strong evidence rather than a proof. Anything sent to the website is sent to a public server, and create_link stores it permanently.

Development

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 runs nix flake check on Linux (x86-64 and ARM) and macOS. A weekly job checks the live alive2.llvm.org API, since a change there is what would break this tool.

To release, set VERSION and push a matching vX.Y.Z tag on main. The Release workflow builds the archives and images with GoReleaser, attests them, publishes the release with its Homebrew formula (which phongndo/homebrew-tap picks up), and lists the version in the MCP Registry. CI runs the same build as a dry run on every push.

License

MIT; see LICENSE.