CHASE MCP Server

Overview Schema Source Related Servers Discussions Admin

merge

Read-onlyIdempotent

Combines multiple assume-guarantee contract viewpoints for the same component, optionally discharging redundant terms so the result can be checked for realizability or synthesized.

Instructions

Merging of two or more viewpoints of the same component (e.g. function and timing): (A1 & A2, (G1 & G2) | !(A1 & A2)).

With discharge, the result keeps the terms of the contracts, (A1 & A2, G1 & G2), which is the same contract, then drops the redundant terms; each test is one model-checking call. Use it before is_realizable or synthesize, which need the terms.

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": "merge"
  }
}

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

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

A3.6/5.0

Behavior4/5

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

Beyond the read-only/idempotent annotations, the description explains the discharge behavior, that redundant terms are dropped, and that each test is a model-checking call. It does not describe the return format, but the annotations already cover the safety profile.

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 short and front-loads the merge semantics and formula, then gives usage guidance. The formal notation is terse but appropriate for the domain.

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 formal-methods contract merge tool with no output schema and five parameters, it explains the operation and one key flag but leaves return-value shape and most parameter semantics implicit. It is adequate but incomplete.

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% for the top-level parameters, and the description only adds meaning for the discharge parameter. It does not explain contracts, name, backend, or timeout, leaving most of the five parameters to the schema alone.

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 specific operation, merging, applied to viewpoints of the same component and gives a formal expression. It does not distinguish the tool from close siblings such as conjoin or compose, but the core purpose is clear.

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?

It explicitly says to use this before is_realizable or synthesize because those tools need the terms, which gives clear usage context. It does not state when not to use it or compare it directly with other merge-like siblings.

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