Skip to main content
Glama
Sign In
CHASE MCP Server

CHASE MCP Server

by chase-cps
OverviewSchemaSourceRelated ServersDiscussionsAdmin
Python
Local

remove_redundant

Read-onlyIdempotent

Removes assumptions and guarantees that are implied by other contract terms, returning the simplified contract and each removed term; terms with unfinished checks are kept.

Instructions

Drop the assumptions implied by the other assumptions, and the guarantees implied by the assumptions and the other guarantees. Returns the contract and the terms removed (removed: each term with its part, and with core the terms that imply it); terms whose check did not finish are kept and listed in unknown. Choose synth by what the contract is for next. false (the default) keeps A -> G: before the algebra and the checks (compose, refines, verify, ...). true keeps realizability and the controllers: before synthesis (is_realizable, synthesize, is_well_separated, is_vacuous); a term is dropped only when it is implied in the GR(1) game, and each removed term has its kind (init, safety, justice). With synth the terms must be GR(1), and there is no context. The two differ only when the assumptions are wrong (unsatisfiable, or constraining the outputs). 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": {
      "contract": "<contract>"
    },
    "name": "remove_redundant"
  }
}

Input Schema

NameRequiredDescriptionDefault
coreNo
synthNo
backendNoauto
contextNo
timeoutNo
contractYes

Schema Changelog

Changes observed during successful MCP inspections.

  1. Changed1 schema field changedv0.7.0
    • addedInput schema / $defs / ContractSpec / properties / constants
      Added value: +{
+  "additionalProperties": {
+    "anyOf": [
+      {
+        "type": "integer"
+      },
+      {
+        "type": "number"
+      }
+    ]
+  },
+  "description": "Named constants: name -> value; the formulas use the names (repair changes them)",
+  "title": "Constants",
+  "type": "object"
+}
  2. Changed7 schema fields changedv0.4.2
    • changedInput schema / $defs / ContractSpec / properties / inputs / 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"
+  }
+]
    • changedInput schema / $defs / ContractSpec / properties / inputs / description
      Previous value: -"Input variables: \"bool\", [low, high], or \"real\""New value: +"Input variables: \"bool\", [low, high], \"real\", or \"word[n]\" (\"signed word[n]\")"
    • changedInput schema / $defs / ContractSpec / properties / outputs / 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"
+  }
+]
    • changedInput schema / $defs / ContractSpec / properties / outputs / description
      Previous value: -"Output variables: \"bool\", [low, high], or \"real\""New value: +"Output variables: \"bool\", [low, high], \"real\", or \"word[n]\" (\"signed word[n]\")"
    • 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"
+]
    • addedInput schema / properties / core
      Added value: +{
+  "default": false,
+  "title": "Core",
+  "type": "boolean"
+}
    • addedInput schema / properties / synth
      Added value: +{
+  "default": false,
+  "title": "Synth",
+  "type": "boolean"
+}
  3. First observedv0.3.1

TDQS

A4.2/5.0
Behavior5/5

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

Annotations already cover read-only/idempotent/closed-world, yet the description adds real behavioral detail: the return payload (`removed` with each term's part and core, plus `unknown` for terms whose check did not finish — a clear timeout/failure semantics), and that synth-mode removal is only valid in the GR(1) game with per-term kinds. It even explains when the two modes diverge (unsatisfiable or output-constraining assumptions).

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?

Front-loaded with the action and the return shape before the parameter guidance, and nearly every sentence carries information (mode semantics, GR(1) constraint, context definition). It is dense and somewhat run-on, with an awkward sentence fragment about GR(1) and no context, but there is little filler to cut.

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

Completeness4/5

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

With no output schema, the description correctly explains what comes back (`removed` with part/core, `unknown`). For a 6-parameter mutation-adjacent tool it covers the semantically hard flags adequately; only backend selection and timeout behavior are left undocumented.

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

Parameters4/5

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

Schema description coverage is 0% for the top-level parameters, so the description carries the burden — and it does for three of them: `core` (attach the terms that imply each removed term), `synth` (mode + GR(1) restriction + no context), and `context` (formulas every behavior satisfies, with an axiom/physical-law example). `backend` and `timeout` are never explained, leaving a gap.

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?

Opens with a specific verb+resource: it drops assumptions implied by other assumptions and guarantees implied by assumptions/guarantees, and returns the contract plus removed terms. That is a precise, non-tautological statement of purpose. It does not explicitly name a sibling it is not (e.g. `simplify`), so sibling differentiation is only implicit.

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

Usage Guidelines4/5

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

Gives concrete routing guidance via the `synth` flag: false for work before the algebra/checks (compose, refines, verify), true for work before synthesis (is_realizable, synthesize, is_well_separated, is_vacuous). It also states the constraint that with synth the terms must be GR(1) and there is no context. What's missing is when to call this at all versus `simplify` or `unsat_core`.

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