CHASE MCP Server

Overview Schema Source Related Servers Discussions Admin

compose

Read-onlyIdempotent

Combines two or more assume-guarantee contracts in parallel, links same-named variables, and can discharge implied assumptions to support refinement checks.

Instructions

Parallel composition of two or more contracts (the contract of the system made of the components). Variables with the same name are connected; no variable can be an output of two contracts.

By default the closed form ((A1 & A2) | !(G1 & G2), G1 & G2). With discharge, the result keeps the terms of the contracts: an assumption of a component implied by the component that drives its inputs is dropped, then the redundant terms; each test is one model-checking call. That result is an abstraction of the composition: a refinement proved on it holds for the composition, a failed one may not.

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": {
      "contracts": "<contracts>"
    },
    "name": "compose"
  }
}

Input Schema

Name	Required	Default
`name`	No
`backend`	No	auto
`timeout`	No
`contracts`	Yes
`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"
+}

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

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

First observedv0.3.1Oct 27, 2026

TDQS

A3.6/5.0

Behavior4/5

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

Annotations already establish this as a read-only, idempotent, closed-world computation, and the description adds genuine behavioral context beyond that: the default output is the closed form ((A1 & A2) | !(G1 & G2), G1 & G2), discharge produces an abstraction with one model-checking call per test, and the abstraction is sound only in the positive direction. It does not state what the returned contract looks like concretely or likely runtime bounds beyond timeout, but the semantic contract is well disclosed.

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 purpose and composition rule are front-loaded, and the second paragraph is dense but every sentence carries distinct information (closed form, discharge behavior, soundness caveat). It is jargon-heavy but not padded.

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 5-parameter computational tool with no output schema and no annotations about failure modes, the description covers the core semantics but omits what the tool actually returns (a new contract object?) and how backend/timeout affect execution. Adequate for an expert, but an agent lacks enough to configure the call confidently.

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?

Schema description coverage is 0% for the top-level parameters, so the description must carry the burden; it does explain the two semantically hard ones — `contracts` (composition semantics, variable connection rule) and `discharge` (keeps terms, drops implied assumptions, abstraction). The remaining `name`, `backend`, and `timeout` parameters get no mention at all (backend selection strategy and timeout units/effect are left to the enum and default), so compensation is only partial.

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?

States a specific operation and resource: 'parallel composition of two or more contracts', with the key semantic rule that variables of the same name are connected and no variable may be an output of two contracts. It does not distinguish itself from siblings such as conjoin, merge, or divide, which also manipulate contracts, so the agent must infer the boundary.

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 explains what the discharge flag changes and its soundness consequence ('a refinement proved on it holds for the composition, a failed one may not'), which is implicit usage guidance for that parameter. However, it never says when to choose compose over conjoin/merge, nor when discharge is worth the abstraction cost versus using the default closed form.

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