Skip to main content
Glama
Sign In
formal-proof-mcp

formal-proof-mcp

by nickharris808
OverviewSchemaSourceRelated ServersDiscussionsAdmin
Python
Local

gate_count

Counts states admitted when a policy check is removed, revealing redundant checks. A zero count means the check is redundant.

Instructions

Exactly how many states does removing a check admit? Replaces 'we found no escapes' with a count. Zero means the check is REDUNDANT, which is a finding. Requires gatecount.

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": {
      "domain": "<domain>",
      "policy": "<policy>",
      "weakened": "<weakened>"
    },
    "name": "gate_count"
  }
}

Input Schema

NameRequiredDescriptionDefault
domainYeseach variable to a list of values or {lo, hi[, step]}
policyYesthe full policy, with the check
weakenedYesthe policy with the check removed

Schema Changelog

Changes observed during successful MCP inspections.

  1. First observedv0.1.0

TDQS

A3.6/5.0
Behavior3/5

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

With no annotations, the description carries the full burden of behavioral disclosure. It usefully reveals that the tool returns a count, that zero indicates redundancy, and that `gatecount` is required. However, it does not specify the exact output format, error behavior, or whether there are any side effects.

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

Conciseness5/5

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

The description is three short sentences with no redundancy. It front-loads the core operation, explains the output interpretation, and notes the external requirement, with every sentence earning its place.

Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.

Completeness4/5

Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?

Given its moderate complexity (three required parameters, nested objects, no output schema, no annotations), the description is nearly complete. It conveys the result semantics and the `gatecount` prerequisite; only the exact return representation and failure behavior are left unstated.

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 100%, with domain, policy, and weakened all described meaningfully. The description adds no parameter-level detail beyond what the schema already provides, so the baseline score of 3 applies.

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?

The description states the tool counts exactly how many states removing a check admits, which is a specific verb-resource-result combination. It also interprets zero as 'REDUNDANT' and explicitly contrasts with the existing 'we found no escapes' output, distinguishing it from sibling check tools.

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?

There is no explicit when-to-use or when-not-to-use guidance. The phrase 'Replaces we found no escapes with a count' hints that this is a count-oriented alternative to a boolean check, but no sibling tool is named and no selection conditions are given.

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