Skip to main content
Glama
Sign In
CHASE MCP Server

CHASE MCP Server

by chase-cps
OverviewSchemaSourceRelated ServersDiscussionsAdmin
Python
Local

implies

Read-onlyIdempotent

Checks whether an LTL formula phi -> psi is valid under given context formulas, returning valid or a counterexample trace.

Instructions

On formulas: validity. Is the LTL formula phi -> psi valid, i.e. true for every behavior? Returns valid, or invalid with a counterexample trace satisfying phi and violating psi. context: formulas that every behavior satisfies (e.g. an axiom of an encoding, a physical law); the behaviors that violate them are left out.

Tool call template

Replace each placeholder with a value matching the input schema. Only required parameters are included; add optional parameters as needed.

{
  "id": 1,
  "jsonrpc": "2.0",
  "method": "tools/call",
  "params": {
    "arguments": {
      "phi": "<phi>",
      "psi": "<psi>",
      "variables": "<variables>"
    },
    "name": "implies"
  }
}

Input Schema

NameRequiredDescriptionDefault
phiYes
psiYes
backendNoauto
contextNo
timeoutNo
variablesYes

Schema Changelog

Changes observed during successful MCP inspections.

  1. Changed2 schema fields changedv0.4.2
    • changedInput schema / properties / backend / enum
      Previous value: -[
-  "auto",
-  "nuxmv",
-  "nusmv"
-]New value: +[
+  "auto",
+  "nuxmv",
+  "nusmv",
+  "nuxmv/ic3",
+  "nuxmv/bdd",
+  "nuxmv/bmc",
+  "nuxmv/portfolio",
+  "nusmv/bdd",
+  "nusmv/bmc"
+]
    • changedInput schema / properties / variables / additionalProperties / anyOf
      Previous value: -[
-  {
-    "enum": [
-      "bool",
-      "real"
-    ],
-    "type": "string"
-  },
-  {
-    "maxItems": 2,
-    "minItems": 2,
-    "prefixItems": [
-      {
-        "type": "integer"
-      },
-      {
-        "type": "integer"
-      }
-    ],
-    "type": "array"
-  }
-]New value: +[
+  {
+    "enum": [
+      "bool",
+      "real"
+    ],
+    "type": "string"
+  },
+  {
+    "maxItems": 2,
+    "minItems": 2,
+    "prefixItems": [
+      {
+        "type": "integer"
+      },
+      {
+        "type": "integer"
+      }
+    ],
+    "type": "array"
+  },
+  {
+    "pattern": "^(signed |unsigned )?word\\[[1-9][0-9]*\\]$",
+    "type": "string"
+  }
+]
  2. First observedv0.3.1

TDQS

B3.3/5.0
Behavior4/5

Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?

Annotations already declare readOnlyHint=true and idempotentHint=true, so the safety profile is covered. The description adds useful behavioral detail beyond annotations: it returns valid or invalid with a counterexample trace satisfying phi and violating psi, and it explains how context formulas suppress violating behaviors.

Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.

Conciseness4/5

Is the description appropriately sized, front-loaded, and free of redundancy?

The description is compact and front-loads the validity question, then covers the return behavior and context semantics. The initial fragment 'On formulas: validity' is slightly awkward, but the overall structure is efficient.

Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.

Completeness2/5

Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?

For a six-parameter solver tool with required nested variables, an enum backend, and no output schema, the description is not complete enough. It helps by explaining the return value and context, but it does not explain variable typing, backend selection, or timeout semantics.

Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.

Parameters2/5

Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?

Schema description coverage is 0%, so the description must carry parameter meaning. It defines phi and psi only through the formula phi -> psi and explains context, but it leaves the required variables parameter, backend choices, and timeout behavior undocumented.

Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.

Purpose4/5

Does the description clearly state what the tool does and how it differs from similar tools?

The description clearly states the specific operation: checking whether the LTL implication phi -> psi is valid for every behavior. It is distinguishable from generic verification tools, but it does not explicitly contrast itself with nearby siblings such as imply, coimply, refines, or verify.

Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.

Usage Guidelines3/5

Does the description explain when to use this tool, when not to, or what alternatives exist?

The description implies the tool should be used when proving validity of an implication and explains what the context parameter means. However, it gives no explicit guidance on when to use this instead of alternatives like verify, is_satisfiable, refines, or imply.

Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.

Deploy Server

Other Tools