monogate-forge-mcp 0.3.0

MCP server exposing the Monogate Forge compiler as 9 tools + REST /compile

monogate-forge-mcp

MCP server that exposes the Monogate Forge EML compiler and the SuperBEST corpus as 8 tools any MCP-compatible client (Claude Desktop, IDE plugins, custom agents) can call. The PyPI distribution is monogate-forge-mcp; the CLI command it installs is forge-mcp.

• Live endpoint: https://mcp.monogate.dev/sse
• Status: https://mcp.monogate.dev/health
• License: Apache-2.0 for this wrapper. Forge engine targets are split Free / Pro -- see list_targets.

Tools

Tool	Tier	Purpose
compile	Free target / Pro target	Compile EML to one Forge target. Pro targets need a license token from monogateforge.com.
profile	Free	Per-function chain order, cost class, fp16 drift risk, FPGA estimates when @target(fpga) is present.
verify	Free	Emit Lean 4 theorem scaffolding with sorry proofs. Does NOT run Lean. Returns {theorems_emitted, sorries, ready_for_lean_check, lean_source} so the caller can run lake build themselves.
search_corpus	Free	Query the 576-record SuperBEST corpus by name/expression substring, domain, or max chain order.
genome	Free	Find structural neighbours in the corpus via cost-class fingerprint distance (wraps eml_cost.find_siblings).
explain_function	Free	Human-readable optimizer trace for one function: passes that fired, before/after node counts, SuperBEST family.
list_targets	Free	Enumerate Forge targets split by Free / Pro tier.
list_verticals	Free	List industry verticals with kernel counts. Sources themselves are not exposed.

The verify tool is honest by contract: it never claims a theorem is "proven", "verified", or "machine-checked". It only emits Lean source you can run yourself.

Run locally

git clone https://github.com/agent-maestro/monogate-forge-mcp
cd monogate-forge-mcp

# Install the wrapper + the Forge engine + cost analyzer.
pip install -e ../forge       # editable install of monogate-forge
pip install -e .

# stdio transport for IDE / Claude Desktop attach
forge-mcp --transport stdio

# SSE transport on http://0.0.0.0:8080
forge-mcp --transport sse

Claude Desktop config

{
  "mcpServers": {
    "forge": {
      "command": "forge-mcp",
      "args": ["--transport", "stdio"]
    }
  }
}

Deploy to Fly.io

The deploy artifacts under deploy/ build the image from the monorepo root so it can COPY both forge/ (the engine) and mcp-server/ (this wrapper) in one shot.

cd ~/monogate                    # monorepo root
fly auth login                   # one-time

# First time: create the Fly app, set the license signing key,
# deploy, and verify /health.
bash mcp-server/deploy/deploy.sh --first-time

# Subsequent deploys:
bash mcp-server/deploy/deploy.sh

After the first deploy, point DNS at the app:

fly certs create -a monogate-forge-mcp mcp.monogate.dev
# then add the CNAME / A+AAAA records `fly` prints

Environment

Var	Purpose	Default
PORT	TCP port to bind. Fly.io sets this.	8080
FORGE_MCP_HOST	Bind address.	0.0.0.0
FORGE_MCP_TRANSPORT	stdio, sse, or streamable-http.	sse
MONOGATE_FORGE_SIGNING_KEY	Override the embedded ed25519 public key used to verify Pro license tokens. Set as a Fly secret in production.	unset

Tests

Three layers, all real (no mocking the engine):

pytest tests/test_auth.py        # 10 license / target-tier tests
pytest tests/test_tools.py       # 25 in-process tool tests
pytest tests/test_server_e2e.py  # 10 e2e tests through the real
                                 # MCP stdio transport

The e2e suite spawns python -m forge_mcp.server --transport stdio in a subprocess and talks JSON-RPC over the official MCP client SDK. This is the closest in-process equivalent to "what Claude sees on the wire" before deployment.

Versioning

monogate-forge-mcp tracks monogate-forge major versions. The engine shipped in the deployed image is whatever pip install /src/forge resolves at image-build time (always the version vendored under forge/ in this monorepo).