Skip to main content
Glama
Sign In
CHASE MCP Server

CHASE MCP Server

by chase-cps
OverviewSchemaSourceRelated ServersDiscussionsAdmin
Python
Local

refines

Read-onlyIdempotent

Checks whether one assume-guarantee contract can replace another by verifying assumption and guarantee implications, returning valid, invalid with a counterexample trace, or unknown.

Instructions

Does refined refine abstract (can it replace it)? Checks that the assumptions of abstract imply those of refined, and that the guarantees of refined imply those of abstract. status is valid, invalid (with failed and a counterexample trace), or unknown. context: formulas that every behavior satisfies (e.g. an axiom of an encoding, a physical law); the behaviors that violate them are left out. Continuous time: when a step is a sample taken every period seconds and each variable changes at most lipschitz per second (one number, or {variable: number}), the refinement is checked between the samples too: what refined assumes and abstract guarantees is made stricter, what is known is made weaker (chase_cps.sampled). Intervals may then be written with times: G[0s,2s], F[0ms,500ms]. The margins are a sufficient condition: valid shows it in continuous time; otherwise the status is unknown (not shown), never invalid; check without lipschitz to see whether it fails at the samples.

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": {
      "refined": "<refined>",
      "abstract": "<abstract>"
    },
    "name": "refines"
  }
}

Input Schema

NameRequiredDescriptionDefault
periodNo
backendNoauto
contextNo
refinedYes
timeoutNo
abstractYes
lipschitzNo

Schema Changelog

Changes observed during successful MCP inspections.

  1. Changed3 schema fields 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"
+}
    • addedInput schema / properties / lipschitz
      Added value: +{
+  "anyOf": [
+    {
+      "type": "number"
+    },
+    {
+      "additionalProperties": {
+        "type": "number"
+      },
+      "type": "object"
+    },
+    {
+      "type": "null"
+    }
+  ],
+  "default": null,
+  "title": "Lipschitz"
+}
    • addedInput schema / properties / period
      Added value: +{
+  "anyOf": [
+    {
+      "type": "number"
+    },
+    {
+      "type": "null"
+    }
+  ],
+  "default": null,
+  "title": "Period"
+}
  2. Changed5 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"
+]
  3. First observedv0.3.1

TDQS

A4.4/5.0
Behavior5/5

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

Annotations only cover read-only/idempotent/closed-world, but the description discloses the outcome space (valid / invalid / unknown), what an invalid result carries (`failed` plus a counterexample trace), and the semantics of `context` (formulas every behavior satisfies; violating behaviors are excluded). It also candidly discloses the soundness limitation of the continuous-time mode — margins are sufficient only, so a non-proof yields unknown, never invalid — which is exactly the kind of behavioral caveat an agent cannot get from structured fields.

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: the core question and the refinement obligation come first, then the status contract, then the optional `context` and continuous-time modes. It is dense — the continuous-time sentence runs long and nests the lipschitz/period rules with an interval-syntax aside — but no sentence is filler, and the internal tool reference `chase_cps.sampled` is the only questionable token.

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?

With no output schema, the description does well on return shape (status values and the counterexample on invalid). For a 7-parameter solver, though, `backend` (9 enum choices) and `timeout` (default 300, units unspecified, and whether a timeout maps to unknown or an error) are left entirely undefined, which are exactly the knobs an agent may need to adjust on a hard verification problem.

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 reported as 0% for the top-level parameters, so the description carries real weight: it defines `context`, the meaning of `period` plus `lipschitz` (number or {variable: number}), and even the resulting interval syntax G[0s,2s]/F[0ms,500ms], and identifies `refined`/`abstract` as the two contracts being compared. `backend` and `timeout` remain entirely unexplained in both schema and description, so compensation is substantial but incomplete.

Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.

Purpose5/5

Does the description clearly state what the tool does and how it differs from similar tools?

States a precise question the tool answers ("Does `refined` refine `abstract` (can it replace it)?") and then spells out the exact semantic obligation in both directions (abstract's assumptions imply refined's, refined's guarantees imply abstract's). This verb+resource phrasing plus the formal definition distinguishes it from the generic implication siblings (`imply`, `implies`, `coimply`) without needing to name them.

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?

The framing "can it replace it?" tells the agent the decision this tool supports, and the closing instruction ("check without lipschitz to see whether it fails at the samples") gives an explicit follow-up workflow when a result is unknown. What is missing is an explicit comparison to the closest siblings, e.g. when to prefer `is_implementation` or `imply` over this contract-level refinement check.

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