Skip to main content
Glama
Sign In
CHASE MCP Server

CHASE MCP Server

by chase-cps
OverviewSchemaSourceRelated ServersDiscussionsAdmin
Python
Local

conjoin

Read-onlyIdempotent

Combines two or more assume-guarantee contracts into a single contract that refines all inputs, optionally discharging guarantees under shared assumptions.

Instructions

Conjunction (greatest lower bound) of two or more contracts: a contract that refines all of them, (A1 | A2, G1 & G2).

With discharge, the result keeps the terms (the same contract): each guarantee under the assumptions of its contract that the others do not imply; with the same assumptions, (A, G1 & G2). 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": {
      "contracts": "<contracts>"
    },
    "name": "conjoin"
  }
}

Input Schema

NameRequiredDescriptionDefault
nameNo
backendNoauto
timeoutNo
contractsYes
dischargeNo

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]\")"
    • 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"
+}
  3. First observedv0.3.1

TDQS

B3.4/5.0
Behavior4/5

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

Annotations already establish read-only and idempotent behavior, so the description does not need to cover safety. It adds useful behavioral detail by explaining what discharge does and noting that each test is one model-checking call, though it does not discuss timeout or backend behavior.

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 three dense sentences with the core purpose front-loaded. The formula notation is somewhat terse but appropriate for a technical contract operation.

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?

The core contract-conjunction semantics and discharge behavior are explained, but important operational details for backend selection, timeout, naming, and the returned result are not covered. With no output schema, the description could do more to set expectations for the result.

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 reported as 0%, so the description must compensate. It only clarifies the contracts count and the discharge semantics, while name, backend, timeout, and the detailed ContractSpec structure are left unexplained or only present in the schema.

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: conjunction/greatest lower bound of two or more contracts, including the resulting formula shape. It is clear what the tool does, though it does not explicitly distinguish itself from closely related siblings such as compose, merge, or disjoin.

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 combination-of-contracts use case is implied, and the discharge option is described, but there is no explicit guidance on when to choose this over alternatives like compose, merge, or disjoin. No exclusions or prerequisites are stated.

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