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

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

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

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 patchalive2-mcp verify -opt upstream -passes gvn repro.ll        # trunk LLVMalive2-mcp verify before.ll after.ll                        # two files, matched by namealive2-mcp get-link -verify https://alive2.llvm.org/ce/z/_kCuTValive2-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, nixfmtgo test -race ./...  # unit tests against a fake Alive2 servernix 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.