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 2026-07-28 over stdio (JSON-RPC 2.0), and only that
revision: clients that need the initialize handshake (2025-11-25 and
earlier) are rejected.
The image bundles the server, Erlang, and the E prover, so the only
prerequisite is Docker. Add the server to your project's .mcp.json:
{
"mcpServers": {
"atp": {
"command": "docker",
"args": ["run", "-i", "--rm", "ghcr.io/jcschuster/atp_mcp:latest"]
}
}
}That gives you SystemOnTPTP (every prover on tptp.org) and a local E
(query_backend with backend: "local_exec") with no configuration.
For Isabelle as well, use the latest-isabelle tag (amd64, a few GB; the
container needs a few GB of RAM for the HOL session). The server starts
Isabelle itself on the first Isabelle call, which takes up to a minute;
later calls in the same session reuse it.
To configure the server, mount your project at /work, where it looks for
atp_mcp.exs, and forward the environment variables
the file reads:
{
"mcpServers": {
"atp": {
"command": "docker",
"args": [
"run",
"-i",
"--rm",
"-v",
"${PWD}:/work:ro",
"-e",
"STAREXEC_USER",
"-e",
"STAREXEC_PASS",
"ghcr.io/jcschuster/atp_mcp:latest"
],
"env": { "STAREXEC_USER": "me", "STAREXEC_PASS": "…" }
}
}
}For Claude Code, also approve the server in .claude/settings.json:
{
"enabledMcpjsonServers": ["atp"]
}To build the images yourself:
docker build -t atp_mcp . # SystemOnTPTP + E
docker build -t atp_mcp:isabelle --target isabelle . # + Isabelle/HOLRelated MCP server: MCP Logic
Without Docker, install the escript (Elixir 1.20 / OTP 29):
mix escript.install hex atp_mcp
export PATH="$HOME/.mix/escripts:$PATH"and use "command": "atp_mcp" in .mcp.json. Local backends then use
whatever is on your PATH: eprover for local_exec, isabelle for the
Isabelle backend.
The escript does not read your project's config/*.exs. It reads one
config file at startup, the first of:
atp_mcp --config PATH;
the ATP_MCP_CONFIG environment variable;
atp_mcp.exs in the working directory — for an MCP host, the project
root (/work in the container).
The file is ordinary Elixir Config, evaluated at startup, so read
secrets from the environment rather than writing them into it:
# atp_mcp.exs
import Config
config :atp_client, :sotptp,
default_system: "Vampire", # a bare name runs the latest version
default_time_limit_sec: 30
config :atp_client, :local_exec,
binary: "vampire",
args: ["--mode", "casc", "-t", "30"],
cpu_timeout_s: 30
config :atp_client, :starexec,
base_url: "https://starexec.example.org/starexec",
username: System.get_env("STAREXEC_USER"),
password: System.get_env("STAREXEC_PASS")Without any configuration:
SystemOnTPTP uses tptp.org and the latest E.
LocalExec runs eprover --auto --tstp-format --cpu-limit=30 if
eprover is on PATH.
Isabelle starts a resident server named atp_mcp on a free port if
isabelle is on PATH, or reuses one that is already running. Outside a
container that server outlives the MCP process, so later sessions skip
the startup cost. Stop it with isabelle server -n atp_mcp -x. To use a
server you run yourself, configure it instead:
config :atp_client, :isabelle,
host: "isabelle.example.org",
port: 9999,
password: System.get_env("ISABELLE_PASSWORD")and set config :atp_mcp, isabelle_autostart: false to rule out a local
one.
StarExec has no defaults; it needs base_url, username, and
password.
See the AtpClient docs for every setting.
atp_mcp doctor prints, for each backend, the settings it resolved to and
whether it is reachable. Run it the way your MCP host runs the server:
$ docker run --rm -v "$PWD:/work:ro" ghcr.io/jcschuster/atp_mcp doctor
atp_mcp 0.8.0
config file: /work/atp_mcp.exs
sotptp - SystemOnTPTP
url: "https://tptp.org/cgi-bin/SystemOnTPTPFormReply"
default_system: "Vampire"
default_time_limit_sec: 30
check: OK
…Name backends to check only those (atp_mcp doctor sotptp local_exec). It
exits with status 1 if any check fails, and passwords are shown only as set
or unset.
AtpClient.Backend)list_backendsLists every backend the server exposes (sotptp, isabelle, local_exec,
starexec) with its human-readable label.
describe_szsReturns a text reference for the
SZS Ontology — the vocabulary every prover verdict
is reported in. Lists every Success status (Theorem, Unsatisfiable,
Satisfiable, CounterSatisfiable, ContradictoryAxioms, …) and NoSuccess
status (GaveUp, Timeout, ResourceOut, MemoryOut, Forced,
InputError, …) with its mnemonic and definition, so an agent can decide
what a verdict means without leaving the MCP session. Generated from
Tptp.Szs.Ontology, the table verdicts are read against. Takes no
arguments.
verify_backendProbes a backend's configuration and reachability. Returns OK or a
descriptive error.
Argument | Type | Required | Description |
| string | yes |
|
Backend-specific override keys (base_url, password, binary, …) are
forwarded through to the backend's verify/1.
query_backendSubmits a TPTP-format problem to any backend through the unified
c:AtpClient.Backend.query/2 entry point and returns an SZS Ontology
verdict (Theorem, Unsatisfiable, Satisfiable, CounterSatisfiable,
GaveUp, Timeout, ResourceOut, …). Call describe_szs for the full
vocabulary.
Argument | Type | Required | Description |
| string | yes |
|
| string | yes | TPTP problem text |
| integer | no | Applied by backends that honour it ( |
| boolean | no | Return the system's verbatim output instead of the SZS verdict |
Per-backend overrides are passed through (e.g. binary for local_exec,
timeout_ms for isabelle, base_url for starexec, and system — the
SystemOnTPTP name of the prover behind a local_exec binary or a starexec
solver, for reading its output).
list_proversLists every theorem prover system available on SystemOnTPTP.
run_proverSubmits a TPTP problem to a specific prover and returns its SZS status.
Argument | Type | Required | Description |
| string | yes | TPTP problem text |
| string | yes | Prover ID from |
| integer | no | Time limit in seconds |
| boolean | no | Return the prover's verbatim output instead of the SZS verdict |
compare_proversRuns the same problem against multiple provers simultaneously and returns all results side by side, one row per requested system in the order given. A bare name shows the version it ran:
Vampire (Vampire---5.0.1): CounterSatisfiable
E---3.5.1: CounterSatisfiable
Nope: not a system on SystemOnTPTP (see list_provers)Argument | Type | Required | Description |
| string | yes | TPTP problem text |
| string[] | yes | Prover IDs or bare names to compare |
| integer | no | Time limit per prover in seconds |
prove_isabelleSubmits 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 prove_tptp.
Session, host, port, and password come from configuration only.
Argument | Type | Required | Description |
| string | yes | Isabelle theory text (full or body only) |
| string | yes | Theory name (also used as the |
| integer | no | Overall |
| boolean | no | Return Isabelle's message text instead of the verdict |
lint_problemRuns syntax and type diagnostics on a TPTP problem. By default combines the
in-process tptp linter (Tptp.analyze/2)
with TPTP4X on SystemOnTPTP; pass backends: ["local"] for the cheap pass
only. TPTP4X is skipped when the local pass already found an error. Each
finding is reported as line:column [severity] (source) message [code],
with the linter's hint where it gives one, followed by the declared symbols
and their types:
2:8 [warning] (tptp) "axim" is not a TPTP formula role [TPTP0401]
hint: expected one of axiom, hypothesis, definition, …
2:12 [error] (tptp4x) Invalid role, exiting [TPTP4X]
Symbols:
plus : $i > $i (declared at 1:14)Argument | Type | Required | Description |
| string | yes | TPTP problem text |
| string[] | no | Subset of |
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.
skills/atp-mcp/SKILL.md is an
Agent Skill that teaches an agent to use these
tools: the TPTP dialects and which provers accept them, a lint-then-prove
workflow, and what each SZS verdict lets it conclude. It also lists tasks
where a prover helps, such as autoformalisation, checking proofs, and
finding counterexamples, so agents reach for the tools unprompted. To use
it with Claude Code, copy the directory into .claude/skills/ in your
project or ~/.claude/skills/.
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_000MCP Tasks (call now, fetch later through a task handle) fit ATP
workflows almost exactly. Revision 2026-07-28 moved them out of the core
protocol into the official extension io.modelcontextprotocol/tasks. Once
MCP hosts support the extension, the long-running tools here should return
tasks, which would also make a StarExec-style submit_job / await_job
pair natural.
MIT.
Submit a TPTP problem to multiple SystemOnTPTP provers simultaneously
and report SZS Ontology verdicts side-by-side. Useful for
cross-checking or finding the fastest prover for a problem class.
Call describe_szs for the vocabulary used in the output.
| Name | Required | Description | Default |
|---|---|---|---|
| problem | Yes | TPTP problem text | |
| system_ids | Yes | Prover IDs or bare system names to compare | |
| time_limit_sec | No | Time limit per prover in seconds |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
With no annotations, the description carries the full disclosure burden. It usefully states that provers run simultaneously and verdicts are reported side-by-side, but it does not explain failure handling, result ordering, cost/resource implications, or what happens when one prover times out.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is three tightly written sentences with the core action and comparative purpose front-loaded. The pointer to describe_szs is a useful, non-redundant addition.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
For a three-parameter execution tool with no output schema, the description adequately explains the high-level return value as side-by-side SZS verdicts and routes agents to describe_szs for vocabulary. Minor gaps remain around failure behavior and per-prover timeout semantics.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema description coverage is 100%, so all parameters are already documented structurally. The description only adds general context about TPTP problems and SystemOnTPTP provers, without adding format details for system_ids or time_limit_sec.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The description states a specific verb and resource: submit a TPTP problem to multiple SystemOnTPTP provers simultaneously and report SZS verdicts side-by-side. It is clearly distinguishable from the sibling run_prover by emphasizing multiple provers and comparative output.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
It gives explicit use cases: cross-checking and finding the fastest prover for a problem class. It also points to describe_szs for interpreting output, though it does not explicitly say when to prefer run_prover or list exclusion conditions.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Return a text description of the SZS Ontology (https://tptp.org/UserDocs/SZSOntology/), the vocabulary every other tool uses to report verdicts. Enumerates each Success status (Theorem, Unsatisfiable, Satisfiable, CounterSatisfiable, …) and NoSuccess status (GaveUp, Timeout, ResourceOut, Forced, …) with a short gloss so an agent can decide what a verdict means without leaving the MCP session.
| Name | Required | Description | Default |
|---|---|---|---|
No parameters | |||
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
No annotations are present, so the description carries the full burden, and it does so reasonably: 'Return a text description' makes clear this is a pure read with no side effects, and it discloses the shape of the payload (Success vs NoSuccess enumerations with short glosses). It does not describe output format in detail (plain text vs structured), which keeps it below 5.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
A single sentence with an embedded URL and a parenthetical list of representative statuses. The purpose is front-loaded in the first clause and every sub-clause (ontology reference, status categories, agent benefit) adds information rather than repeating the name.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
With no annotations and no output schema, the description must explain both what it does and roughly what comes back, and it does both by naming the two status categories and giving examples. It only falls short of 5 because it doesn't indicate the output's format or size, which an agent might reasonably want for a describing tool.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
The tool takes zero parameters, so the baseline of 4 applies. Nothing in the description is needed to clarify inputs, and nothing misleading is said about them.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
States a specific verb and resource ('Return a text description of the SZS Ontology') and additionally explains that this is the shared verdict vocabulary used by every other tool. That framing lets an agent distinguish it from siblings like list_provers or run_prover without opening the schema.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
The description implies usage clearly: consult this to interpret verdicts produced by other tools ('so an agent can decide what a verdict means without leaving the MCP session'). It does not name an alternative or an explicit when-not-to-call condition, but for a zero-parameter reference tool there is little ambiguity about when it applies.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Run 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.
| Name | Required | Description | Default |
|---|---|---|---|
| problem | Yes | TPTP problem text | |
| backends | No | Which lint backends to run (default: both) |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
With no annotations, the description carries the full behavioral burden. It usefully discloses that the default combines an in-process structural checker with TPTP4X on SystemOnTPTP and that local is the cheap pass, but it omits return format, external-service implications, timeout/error behavior, and resource costs.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
Two sentences, front-loaded with the core action and followed by the default/backend tradeoff. Every sentence adds useful information with no repetition or wasted phrasing.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
For a low-complexity, two-parameter diagnostic tool with full schema coverage, it covers purpose and backend selection adequately. But with no output schema, the description should ideally state what diagnostics are returned and whether results are structured, so the agent knows what to expect.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema coverage is already 100%, so the baseline is 3. The description earns an extra point by explaining the practical meaning behind the backends parameter: default means combining local structural checking with TPTP4X, while local-only is the cheap pass.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The description states a specific verb and resource: "Run syntax and type diagnostics on a TPTP problem." This clearly distinguishes it from prover-running siblings, though it does not explicitly contrast it with tools like verify_backend or query_backend.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
It explains the default backend behavior and when to pass backends: ["local"] for the cheap pass, which is useful parameter-level guidance. However, it does not say when to use this tool versus other diagnostic or verification siblings, nor does it state explicit exclusions.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
List the AtpClient backends this MCP server exposes (sotptp, isabelle, local_exec, starexec) and their human-readable labels.
| Name | Required | Description | Default |
|---|---|---|---|
No parameters | |||
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
No annotations exist, so the description carries the burden. It is inherently a read-only enumeration and implies no side effects, but it does not explicitly state that it is non-mutating, whether the set is static, or what ordering/shape the returned labels take.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
A single front-loaded sentence with no filler; the enumerated backend names earn their place by making the output set concrete.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
With no output schema, the description does the right thing by stating what is returned ('backends ... and their human-readable labels'). It stops short of describing the response shape or ordering, but for a zero-parameter discovery tool this is nearly complete.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
The tool takes zero parameters, so there is nothing for the description to disambiguate beyond what the empty schema already shows; baseline of 4 applies.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
Specific verb 'List' plus concrete resource 'AtpClient backends', with the value set enumerated (sotptp, isabelle, local_exec, starexec). It does not distinguish itself from the similar-shaped sibling list_provers, so an agent must infer the difference between listing backends vs. provers.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
Usage is implied: this is a discovery/enumeration tool for backend identifiers. There is no explicit statement of when to call it versus list_provers, nor any prerequisite or exclusion guidance, leaving routing between sibling list tools partly to inference.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
List every theorem prover system available on SystemOnTPTP.
| Name | Required | Description | Default |
|---|---|---|---|
No parameters | |||
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
No annotations are provided, so the description carries the full burden. "List" implies a safe read, and the source (SystemOnTPTP) is disclosed, but return format, whether entries are IDs or full metadata, and any pagination or availability caveats are not described.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
A single front-loaded sentence with zero waste. The scope word "every" and the source system both earn their place.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
For a zero-parameter listing tool with no output schema, the description is nearly sufficient: it tells an agent what will be listed and from where. It leaves the shape of the returned list implicit, which is a minor gap only.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
The tool takes zero parameters, so there are no parameter semantics to document. Baseline 4 applies; nothing in the description is needed or misleading here.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
States a specific verb (List) and resource (theorem prover systems), plus the source system (SystemOnTPTP) and scope (every). It does not explicitly differentiate from sibling list_backends or compare_provers, but the resource is unambiguous.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
Usage is implied: an agent discovers available provers before calling run_prover or compare_provers. There is no explicit guidance on when to prefer this over list_backends or when not to use it.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Submit a hand-written Isabelle/HOL theory to the Isabelle server
configured for this MCP server. The theory text is written into the
configured shared directory and processed via use_theories on the
long-lived session held by AtpMcp.IsabelleSession (session name,
host, port, and credentials all come from application config — they
are fixed for the lifetime of the server and cannot be overridden
per call). For TPTP/THF problems use query_backend with
backend: "isabelle" instead — that routes through prove_tptp on
the same shared session.
| Name | Required | Description | Default |
|---|---|---|---|
| raw | No | Return the system's verbatim output instead of the SZS verdict | |
| theory | Yes | Isabelle theory text | |
| timeout_ms | No | Overall use_theories timeout in milliseconds | |
| theory_name | Yes | Theory name (also used as the .thy filename) |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
With no annotations, the description carries substantial behavioral context: it discloses that theory text is written into a shared directory, processed on a long-lived `AtpMcp.IsabelleSession`, and that host/port/credentials are fixed per server. It does not fully explain overwrite behavior, failure modes, or return values beyond the `raw` parameter hint.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is front-loaded with the core action, then gives the relevant execution mechanics, then routes TPTP/THF users elsewhere. The three sentences are dense but each serves a clear purpose.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
For a no-annotation, no-output-schema proof submission tool, the description covers purpose, side effects, fixed session configuration, and the key alternative route. It is nearly complete, though it does not explicitly describe expected output or failure/overwrite behavior.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema description coverage is 100%, so the four parameters are already documented in the schema. The description adds context about theory submission and session configuration but does not add parameter-level semantics beyond what the schema provides.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The description states a specific verb and resource: submit a hand-written Isabelle/HOL theory to the configured Isabelle server. It also distinguishes this from the sibling route for TPTP/THF problems via `query_backend` with `backend: "isabelle"`.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
It explicitly says when to use this tool: hand-written Isabelle/HOL theories. It also names the alternative for TPTP/THF problems and the exact sibling tool and parameter to use instead.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Run a TPTP-format problem through any AtpClient backend and return the
normalised SZS Ontology verdict (Theorem, Unsatisfiable, Satisfiable,
CounterSatisfiable, GaveUp, Timeout, ResourceOut, …). The unified
AtpClient.Backend.query/2 entry point — each backend hides its
ceremony (session, prover selection, theory bookkeeping) behind this
call. Call describe_szs for the full ontology.
| Name | Required | Description | Default |
|---|---|---|---|
| raw | No | Return the system's verbatim output instead of the SZS verdict | |
| backend | Yes | Which backend to run on | |
| problem | Yes | TPTP problem text | |
| time_limit_sec | No | Time limit for backends that honour it (sotptp) |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
With no annotations, the description carries the full burden. It usefully discloses that backends abstract away session, prover selection and theory bookkeeping, and enumerates the possible verdict classes including Timeout and ResourceOut, which hints at failure behaviour. It says nothing about remote execution cost (starexec), latency, or what happens when a backend is unavailable.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
Front-loaded with the action and result type, and every sentence is relevant. The trailing 'Call describe_szs' pointer is a small but legitimate addition rather than padding.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
A four-parameter, unannotated tool with no output schema: the description covers outcome classes and points to describe_szs for the ontology, which is helpful. It stops short of describing return shape for the raw flag, error/exception behaviour, or any backend prerequisites, which are needed for confident invocation.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema description coverage is 100%, so backend, problem, raw and time_limit_sec are already documented, which sets the baseline at 3. The description adds only a general note that backends differ in ceremony and does not explain backend-specific behaviour differences beyond what the enum conveys.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
States a specific verb and resource: run a TPTP problem through any AtpClient backend and return the normalised SZS verdict, and names the entry point query/2. It does not differentiate itself from run_prover or compare_provers, which occupy similar territory, so an agent still has to guess which one to pick.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
There is no statement of when to use this versus run_prover, compare_provers or prove_isabelle, despite strong overlap. The only routing hint ('Call describe_szs for the full ontology') points at a helper for verdict semantics, not at an alternative execution path.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Submit a TPTP-format problem to a specific prover on SystemOnTPTP.
Returns the SZS Ontology verdict (Theorem, Unsatisfiable, Satisfiable,
CounterSatisfiable, GaveUp, Timeout, ResourceOut, …) or raw output.
Call describe_szs for the full ontology.
| Name | Required | Description | Default |
|---|---|---|---|
| raw | No | Return the system's verbatim output instead of the SZS verdict | |
| problem | Yes | TPTP problem text | |
| system_id | Yes | Prover ID from list_provers ("Vampire---5.0.1"), or a bare system name ("Vampire") for the latest version offered | |
| time_limit_sec | No | Time limit in seconds |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
With no annotations, the description carries the load and does disclose the return shape (SZS verdict vs raw output) plus notable failure verdicts (Timeout, ResourceOut, GaveUp) an agent must handle. It omits rate limits, remote-service error behavior, and whether calls are billed/slow, so it stops short of full disclosure.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
Three sentences, front-loaded with the action and resource, and the verdict enumeration is genuinely informative rather than filler. The trailing ellipsis list is slightly loose but earns its place by signalling the range of outcomes.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
With no output schema, the description compensates by naming the return type and example verdicts, and all parameters are schema-documented. Missing pieces are minor: no default time limit, no note on output size or what happens with invalid TPTP (lint_problem exists but is not referenced).
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema coverage is 100%, so all four parameters including the raw flag and system_id format are documented in the schema itself. The description only reinforces 'TPTP-format problem' and the raw-output alternative, adding little beyond what the schema already says, so baseline 3 applies.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
States a specific verb ("Submit") and resource ("TPTP-format problem to a specific prover on SystemOnTPTP"), and the singular prover framing separates it from compare_provers and prove_isabelle. An agent can tell immediately what it does and what it returns.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
The 'Message' cross-reference to describe_szs covers how to interpret the returned verdict, which is useful context. However, there is no explicit guidance on when to pick this over compare_provers or prove_isabelle, or what to do when a prover returns GaveUp; usage is only implied by the single-prover framing.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Probe a backend's configuration and reachability. Returns "OK" if the backend is wired up correctly, otherwise an error describing what is missing or unreachable.
| Name | Required | Description | Default |
|---|---|---|---|
| backend | Yes | Backend to probe |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
With no annotations, the description carries the full burden. It does disclose the return contract ("OK" vs. an error describing what is missing or unreachable), which is genuinely useful. It does not say whether the probe mutates anything, how long it may block on an unreachable backend, or whether it requires credentials.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
Two short sentences, front-loaded with the action and resource, and no filler. The return-value clause is load-bearing rather than padding. Slightly below 5 only because the return contract could be stated more crisply in one clause.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
For a one-parameter tool with full schema coverage and no output schema, the description covers the essentials: what it inspects and what it returns on success and failure. The remaining gap is operational (timeouts, side effects), which matters less for an evidently read-only probe.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema description coverage is 100% and the single parameter is a documented enum of four backend names, so the schema does the heavy lifting. The description adds no semantics beyond it — nothing about the difference between checking configuration versus reachability, or what the enum members imply.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
States a specific verb and resource: 'Probe a backend's configuration and reachability.' That distinguishes it from list_backends (enumeration), query_backend (querying), and run_prover (execution) without needing the schema. It does not explicitly name a sibling it is not, which keeps it below a 5.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
Usage is implied rather than stated: a probe that returns 'OK' or an error explains what is missing reads as a pre-flight/diagnostic check. There is no explicit 'use this before run_prover' or 'use query_backend instead when...' guidance, leaving the agent to infer when to reach for it.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Recent tool additions, removals, and schema changes observed during successful MCP inspections.
v0.8.1compare_proversdescribe_szslint_problemlist_backendslist_proversprove_isabellequery_backendrun_proververify_backendScored across 9 tools
Most tools have clearly distinct roles, but `query_backend` and `run_prover` both submit a TPTP problem and return SZS verdicts, differing mainly by abstraction level and target. The descriptions help clarify when to use `prove_isabelle` versus `query_backend` with the Isabelle backend, but there is still some potential for confusion between the unified query path and the direct prover path.
All tools use a consistent snake_case verb_noun pattern (`list_backends`, `verify_backend`, `query_backend`, `run_prover`, `compare_provers`, etc.). Proper nouns and acronyms like `szs` and `isabelle` are used naturally without breaking the convention.
Nine tools is well-scoped for an ATP integration server covering discovery, verification, execution, comparison, linting, and Isabelle-specific proving. Each tool appears to earn its place without obvious redundancy.
The surface covers the core ATP lifecycle well: listing backends/provers, understanding SZS verdicts, verifying configuration, running and comparing provers, linting problems, and proving Isabelle theories. Minor gaps remain around managing or inspecting the long-lived Isabelle session and retrieving raw output consistently across all execution paths.
Zero-trust logic judge: your AI writes a claim as a ZFL table, the ZTL core judges it.
Jailbreak-proof AI guardrails. Automated Reasoning SMT solver, not an LLM. ZK proofs included.
121 machine-proven math facts, plus 49 real-world claims with machine-checked arithmetic
Check claims against a fact-store: consistent, contradicts, or unverifiable — with a receipt.