AtpMcp

An MCP server that exposes AtpClient's four theorem-prover backends — SystemOnTPTP, StarExec, Isabelle, and LocalExec — as tools for Claude Code and other MCP hosts.

Speaks MCP revision 2025-11-25 over stdio (JSON-RPC 2.0).

Installation

mix escript.install hex atp_mcp

This places the atp_mcp binary in ~/.mix/escripts/. Make sure that directory is on your PATH:

export PATH="$HOME/.mix/escripts:$PATH"

Configuration

Add the server to your project's .mcp.json:

{
  "mcpServers": {
    "atp": {
      "command": "atp_mcp"
    }
  }
}

For Claude Code, also approve it in .claude/settings.json:

{
  "enabledMcpjsonServers": ["atp"]
}

Tools

Cross-backend (unified AtpClient.Backend)

list_backends

Lists every backend the server exposes (sotptp, isabelle, local_exec, starexec) with its human-readable label.

verify_backend

Probes a backend's configuration and reachability. Returns OK or a descriptive error.

Backend-specific override keys (base_url, password, binary, …) are forwarded through to the backend's verify/1.

query_backend

Submits a TPTP-format problem to any backend through the unified c:AtpClient.Backend.query/2 entry point and returns the normalized SZS result (Theorem, Satisfiable, Timeout, Out of resources, …).

Per-backend overrides are passed through (e.g. binary for local_exec, session/host/port for isabelle, base_url for starexec).

SystemOnTPTP

list_provers

Lists every theorem prover system available on SystemOnTPTP.

run_prover

Submits a TPTP problem to a specific prover and returns its SZS status.

compare_provers

Runs the same problem against multiple provers simultaneously and returns all results side by side.

Isabelle

prove_isabelle

Submits a hand-written Isabelle/HOL theory to a configured Isabelle server. The theory text is written into the configured shared directory and processed via use_theories. For TPTP/THF problems, use query_backend with backend: "isabelle" instead — that routes through query_tptp.

Diagnostics

lint_problem

Runs syntax and type diagnostics on a TPTP problem. By default combines the in-process structural checker with TPTP4X on SystemOnTPTP; pass backends: ["local"] for the cheap pass only.

Example

Once the MCP server is active, you can ask Claude Code things like:

"Which provers on SystemOnTPTP can prove this TPTP problem? Compare Vampire, E, and Satallax."

Claude will call compare_provers directly and report the SZS results.

"Run this problem against my local E build, then sanity-check it on SystemOnTPTP."

Claude will call query_backend twice — once with backend: "local_exec", once with backend: "sotptp" — and compare the verdicts.

Configuration via config.exs

Backend connection settings are read from AtpClient configuration:

config :atp_client, :sotptp,
  url: "https://tptp.org/cgi-bin/SystemOnTPTPFormReply",
  default_time_limit_sec: 30

config :atp_client, :isabelle,
  host: "isabelle.example.org",
  port: 9999,
  password: System.get_env("ISABELLE_PASSWORD"),
  local_dir: "/shared/problems",
  session: "HOL"

config :atp_client, :local_exec,
  binary: "eprover",
  args: ["--auto", "--tstp-format", "--cpu-limit=10"],
  cpu_timeout_s: 10

config :atp_client, :starexec,
  base_url: "https://starexec.example.org/starexec",
  username: System.get_env("STAREXEC_USER"),
  password: System.get_env("STAREXEC_PASS")

See the AtpClient docs for the full configuration surface.

Cancellation and progress

Long-running tool calls run inside their own Task. The MCP host can:

• Send notifications/cancelled with the in-flight request id to abort a call. Each AtpClient backend tears down its upstream work on caller death:

  • LocalExec SIGKILLs the prover binary via Port closure.
  • StarExec issues DELETE against the remote job.
  • Isabelle drops the session, which aborts the in-flight use_theories task on the server.
  • SystemOnTPTP closes the local connection, but the remote prover runs to its :time_limit_sec — SOTPTP has no remote-cancel endpoint.

• Set _meta.progressToken on tools/call to receive periodic notifications/progress frames while the call is in flight. The heartbeat fires every five seconds by default; override via:

  config :atp_mcp, heartbeat_ms: 10_000
  

Forward note: MCP experimental Tasks primitive

The 2025-11-25 MCP revision incubates an experimental Tasks primitive (call-now / fetch-later, with a task handle for status polling and deferred result retrieval). That maps onto ATP workflows almost exactly. When the primitive stabilises, the long-running tools here should grow a task-returning variant, and a StarExec-style submit_job / await_job pair becomes natural to add.

License

MIT.