CHASE MCP Server

Overview Schema Source Related Servers Discussions Admin

unsat_core

Read-onlyIdempotent

Computes a minimal unsatisfiable core for LTL formulas or assume-guarantee contracts, showing whether assumptions, guarantees, or both contradict; returns none if they can hold together.

Instructions

On formulas: a minimal set of terms that cannot hold together. Give a contract (its assumptions and guarantees, A & G, are searched: the core says whether the assumptions contradict each other, the guarantees do, or the guarantees cannot hold when the assumptions do), or formulas with their variables. status is found with core, none when they can hold together, or unknown with the reason. context: formulas that every behavior satisfies (e.g. an axiom of an encoding, a physical law); the behaviors that violate them are left out.

Tool call template

This tool declares no required parameters. Add optional parameters from the input schema as needed.

{
  "id": 1,
  "jsonrpc": "2.0",
  "method": "tools/call",
  "params": {
    "arguments": {},
    "name": "unsat_core"
  }
}

Input Schema

Name	Required	Default
`backend`	No	auto
`context`	No
`timeout`	No
`contract`	No
`formulas`	No
`variables`	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"
+}

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

changedInput schema / properties / variables / anyOf

Previous value: -[
-  {
-    "additionalProperties": {
-      "anyOf": [
-        {
-          "enum": [
-            "bool",
-            "real"
-          ],
-          "type": "string"
-        },
-        {
-          "maxItems": 2,
-          "minItems": 2,
-          "prefixItems": [
-            {
-              "type": "integer"
-            },
-            {
-              "type": "integer"
-            }
-          ],
-          "type": "array"
-        }
-      ]
-    },
-    "type": "object"
-  },
-  {
-    "type": "null"
-  }
-]New value: +[
+  {
+    "additionalProperties": {
+      "anyOf": [
+        {
+          "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"
+        }
+      ]
+    },
+    "type": "object"
+  },
+  {
+    "type": "null"
+  }
+]

First observedv0.3.1Oct 27, 2026

TDQS

C2.7/5.0

Behavior3/5

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

The annotations already declare read-only, idempotent behavior, and the description adds useful behavioral context: it states that status is 'found with core,' 'none when they can hold together,' or 'unknown with the reason,' and explains that behaviors violating `context` are excluded. It does not discuss backend behavior, timeouts, or computational limits.

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

Conciseness3/5

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

The description is not excessively long, but its structure is awkward: the contract explanation is buried in a dense parenthetical and the sentences are hard to parse. It front-loads the core idea, but the phrasing could be substantially cleaner.

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-verification tool with no output schema, the description covers the central concepts—contract mode, formula mode, status outcomes, and context filtering—well enough for basic use. It still leaves important operational details missing, including backend selection, timeout behavior, and the exact shape of the returned core.

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% across six parameters, so the description must compensate. It gives meaningful semantics for `contract`, `formulas`/`variables`, and `context`, but completely omits `backend` and `timeout`, leaving two parameters unexplained beyond their raw schema defaults/enums.

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

Purpose3/5

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

The description defines an unsat core as 'a minimal set of terms that cannot hold together' and indicates it works over contracts or formulas, so the general purpose is inferable. However, it is phrased as a dense formal note rather than a clear verb-plus-resource statement, and it does not plainly distinguish this tool from siblings such as unrealizable_core or is_consistent.

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?

The only usage guidance is 'Give a contract ... or formulas with their variables,' which describes input modes rather than when to choose this tool over alternatives. There is no explicit when-to-use, when-not-to-use, or sibling routing guidance despite many closely related tools in the list.

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