CHASE MCP Server

Overview Schema Source Related Servers Discussions Admin

divide

Read-onlyIdempotent

Computes the missing contract C such that composing a given part with C refines the target system, with optional discharge of redundant assumptions and guarantees.

Instructions

The contract of the missing component: the largest contract C such that part composed with C refines system. (A & G', (G & A') | !(A & G')).

With discharge, the result keeps the terms: it assumes the assumptions of system and the guarantees of part (under the assumptions of part that system does not give), and guarantees the guarantees of system and the assumptions of part. It is the same contract, then the redundant terms are dropped; each test is one model-checking call.

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": {
      "system": "<system>",
      "part": "<part>"
    },
    "name": "divide"
  }
}

Input Schema

Name	Required	Default
`name`	No
`part`	Yes
`system`	Yes
`backend`	No	auto
`timeout`	No
`discharge`	No

Schema Changelog

Changes observed during successful MCP inspections.

Changed1 schema field changedv0.7.0Nov 2, 2026

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"
+}

Changed7 schema fields changedv0.4.2Oct 29, 2026

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]\")"

addedInput schema / properties / backend

Added value: +{
+  "default": "auto",
+  "enum": [
+    "auto",
+    "nuxmv",
+    "nusmv",
+    "nuxmv/ic3",
+    "nuxmv/bdd",
+    "nuxmv/bmc",
+    "nuxmv/portfolio",
+    "nusmv/bdd",
+    "nusmv/bmc"
+  ],
+  "title": "Backend",
+  "type": "string"
+}

addedInput schema / properties / discharge

Added value: +{
+  "default": false,
+  "title": "Discharge",
+  "type": "boolean"
+}

addedInput schema / properties / timeout

Added value: +{
+  "default": 60,
+  "title": "Timeout",
+  "type": "number"
+}

First observedv0.3.1Oct 27, 2026

TDQS

C2.9/5.0

Behavior3/5

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

Annotations already declare readOnlyHint, idempotentHint and openWorldHint=false, so safety is covered. The description does add real behavioral context — that discharge triggers one model-checking call per test and that redundant terms are dropped from the result — but it never states cost/timeouts, failure behavior when no such component exists, or what the return object looks like.

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

Conciseness2/5

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

It opens with an abstract noun phrase rather than a plain statement of what is computed, then embeds a cryptic formula fragment '(A & G', (G & A') | !(A & G'))' that earns nothing for an agent. The second paragraph is a run-on with garbled phrasing ('It is the same contract, then the redundant terms are dropped'), so the useful facts are buried.

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

Completeness3/5

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

For a six-parameter, no-output-schema operation over nested ContractSpec objects, the description explains the core algebra and discharge behavior but omits the return shape, possible null/empty component outcomes, backend selection rationale, and timeout implications. It is enough for a domain expert, not enough for a general agent.

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

Parameters3/5

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

With 0% schema description coverage at the top level, the description must compensate. It does explain the semantics of 'system' and 'part' and the effect of 'discharge', but leaves 'name', 'backend' (an enum with nine options) and 'timeout' completely undocumented in both schema and prose.

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 states a precise mathematical purpose: compute the largest contract C such that 'part composed with C refines system', which is a specific verb-like operation on a named resource. It implicitly relates to the compose/refines siblings, but never names or contrasts them explicitly, so an agent must already know the domain to place it.

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

Usage Guidelines2/5

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

There is no explicit 'use this when' guidance and no mention of alternatives such as separate, merge, conjoin, or compose, despite a crowded sibling set of similar contract algebra operations. Usage is only inferable from the formal definition, which is exactly the ambiguity an agent needs resolved.

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