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

formal-proof-mcp

by nickharris808
OverviewSchemaSourceRelated ServersDiscussionsAdmin
Python
Local

state_floor

Compute the minimum number of states a system must distinguish to answer a question about its past, then optionally prove a given budget cannot meet that floor. Use to verify state-budget constraints.

Instructions

How many states must a system distinguish to answer a question about its past? An exact count over an enumerated situation space. Optionally proves a state budget cannot meet it. Requires floorgen.

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": {
      "variables": "<variables>",
      "answers": "<answers>"
    },
    "name": "state_floor"
  }
}

Input Schema

NameRequiredDescriptionDefault
answersYesrows of {when: {...}, answer: ...}
defaultNoanswer for unmatched situations
variablesYeseach variable to its finite domain (a list)
has_defaultNo
budget_statesNoif given, also test this budget for impossibility

Schema Changelog

Changes observed during successful MCP inspections.

  1. First observedv0.1.0

TDQS

C2.9/5.0
Behavior2/5

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

With no annotations, the description carries the full burden. It does disclose that the tool computes an exact count, can test a budget, and requires floorgen, but it omits any mention of return format, side effects, failure modes, or whether this is a safe read-only operation.

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 sentences and reasonably compact. The opening rhetorical question is slightly stylistic but not wasteful, and the key capabilities are stated efficiently.

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

Completeness2/5

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

There is no output schema, and the description does not explicitly state what the tool returns, though 'exact count' and 'proves' hint at outputs. It also does not clarify the semantics of default/has_default or the nature of the floorgen dependency, leaving notable gaps for a tool with five parameters and nested objects.

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 coverage is 80%, so the schema already documents most parameters. The description adds some context by referring to an 'enumerated situation space' and 'state budget', which loosely map to variables/answers and budget_states, but it does not meaningfully extend the schema's parameter descriptions.

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 the tool computes an exact state count over an enumerated situation space and optionally proves a given state budget is insufficient. This is a clear, specific action on a defined resource, though it does not explicitly differentiate it from sibling tools such as bound or gate_count.

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 guidance on when to use this tool versus its siblings, nor any exclusions or alternatives. The description implies usage through 'Requires floorgen' and the problem statement, but an agent is left to infer the appropriate context.

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