Skip to main content
Glama
nickharris808

formal-proof-mcp

formal-proof-mcp

Your agent says it proved the theorem. Did anything actually check?

tests License Python Dependencies MCP

Six verification tools over the Model Context Protocol, with one invariant running through all of them:

A result that was not checked is never returned as a result that passed.

Not yet on PyPI. The command below is the one that works today. It installs from this repository, pinned to a tag.

pip install "git+https://github.com/nickharris808/formal-proof-mcp@v0.1.0"

pip install formal-proof-mcp is the intended command once the name is published. It 404s today, which is why it is not the first step above. The tag is pinned rather than @main so a reader installs the exact code this README documents.

Why this exists

Coding agents are fluent about correctness. They will tell you a proof went through, a bound holds, a graph is deadlock-free — and the failure mode is not that they lie, it is that nothing on the other end ever ran. A missing Lean toolchain, an uninstalled dependency, an empty input: each returns something, and "something" reads as success.

So every response here carries status, and the three values are kept strictly apart:

status

meaning

ok

the check ran and passed

failed

the check ran and failed — with the real error attached, for the repair loop

unavailable

the check could not run. Explicitly not a pass.

An agent that reads "no Lean toolchain installed" as "no errors found" will confidently assert a proof it never checked. This server makes that confusion impossible to express.

Related MCP server: prova-mcp

The check that matters most

lake build exits 0 on a development riddled with sorry. Lean accepts the placeholder, compiles happily, and reports success. Compiling is necessary and nowhere near sufficient — only #print axioms reveals what a theorem actually rests on:

$ formal-proof-mcp --selftest
  ok    clean axioms accepted
  ok    sorryAx caught
  ok    empty audit FAILS rather than passing quietly
  ok    0-of-250 bounded at ~1.2%
  ok    acyclic graph certified
  ok    cycle caught with its path
  ok    non-decreasing rank caught
  ok    unknown tool fails loudly
  ok    tools/list returns all six

  lean toolchain: present

selftest passed.

Note line 3. An axiom audit over empty input fails. A coverage tool that cannot cover anything must never pass quietly — that is how an entire corpus goes unaudited while CI stays green.

Install

Not yet on PyPI. pip install formal-proof-mcp is the intended install once published; until then install from the repository — it works exactly the same:

pip install git+https://github.com/nickharris808/formal-proof-mcp@main
pip install formal-proof-mcp                 # zero dependencies

cert_verify and residency_check delegate to signoff-cert and kvleak. Neither is on PyPI, so neither can be an extra: pip ignores an undeclared extra with a warning and exits 0, which would leave you believing those two tools were enabled when they are not. Install them explicitly instead, and only if you want them:

pip install "signoff-cert @ git+https://github.com/nickharris808/signoff-cert@v1.0.1"
pip install "kvleak @ git+https://github.com/nickharris808/kvleak@v0.1.0"

Without them the server runs fine and both tools report unavailable — never a pass.

30-second quickstart

formal-proof-mcp --selftest      # prove each tool actually fires
formal-proof-mcp --list-tools    # the ten tools
formal-proof-mcp                 # serve MCP over stdio

Wire it into Claude Desktop or Cursor:

{
  "mcpServers": {
    "formal-proof": { "command": "formal-proof-mcp" }
  }
}

The ten tools

tool

what it answers

lean_check

Does this Lean 4 source compile? On failure, returns the compiler's own error so the agent repairs its proof instead of asserting one.

axiom_audit

What does the theorem actually rest on? Catches sorryAx and anything outside the allowlist.

bound

What does a k-of-n record support? Exact one-sided Clopper–Pearson. "It passed every time" is not a bound.

gridlock_check

Can this wait-for relation wedge? Returns the actual cycle, and optionally checks a strictly decreasing rank.

cert_verify

Is this signoff-cert/v1 certificate real, with its false-pass bound recomputed from the evidence?

residency_check

Could a cross-tenant cache probe on this model even be interpreted?

Added in 0.2 — the rest of the portfolio

Each of these delegates to a sibling package. If that package is not installed the result is unavailable, never ok — an agent reading "not installed" as "checked and fine" is the exact failure this server exists to prevent, and a missing optional dependency is the likeliest way to produce it. There is a test that blocks the import and asserts the status.

tool

question

needs

prereg_check

can this experiment's decision rule come out both ways?

preregister

state_floor

how many states must the system distinguish?

floorgen

gate_count

exactly how many states does removing this check admit?

gatecount

evidence_audit

run every applicable verifier over a tree, aggregate to one verdict

evidence

Not yet on PyPI. pip install formal-proof-mcp is the intended install once published; until then install from the repository — it works exactly the same:

pip install git+https://github.com/nickharris808/formal-proof-mcp@main
pip install "formal-proof-mcp[portfolio]"     # the server plus evidence-runner

evidence-runner is the one of these four that is on PyPI, so it is the only one an extra can honestly promise. The other three install from a pinned tag:

pip install "preregister @ git+https://github.com/nickharris808/preregister@v0.1.0"
pip install "floorgen    @ git+https://github.com/nickharris808/floorgen@v0.1.0"
pip install "gatecount   @ git+https://github.com/nickharris808/gatecount@v0.1.0"

prereg_check is the one to reach for first. An agent about to run an experiment can be told, before it burns a GPU hour, that its rule cannot fail:

{"decision_rule": "argmax_flips > 0",
 "metrics": {"argmax_flips": {"type": "integer", "lo": 0, "hi": 0}}}
{"status": "failed", "verdict": "UNFALSIFIABLE",
 "explanation": "THE FINDING CAN NEVER BE REPORTED. ... The run is guaranteed to return the null
                 before any data is collected."}

Worked example — driving it the way a client does

Pipe JSON-RPC in, read JSON-RPC out:

$ printf '%s\n' \
  '{"jsonrpc":"2.0","id":1,"method":"initialize","params":{}}' \
  '{"jsonrpc":"2.0","id":2,"method":"tools/call","params":{"name":"gridlock_check",
    "arguments":{"edges":[["a","b"],["b","c"],["c","a"]]}}}' \
  | formal-proof-mcp
initialize -> {'name': 'formal-proof-mcp', 'version': '0.1.0'} 2024-11-05
id=2 isError=True status=failed  wait-for cycle: a -> b -> c -> a

And the audit that catches an assumed theorem:

id=2 isError=True status=failed
  1 theorem(s) depend on sorryAx: these are ASSUMED, not proved, and the development
  still compiles

isError is how the agent learns a check failed rather than merely returned, and the cycle comes back as a path so the answer is actionable rather than a bare boolean.

Honest limits

  • lean_check needs a Lean toolchain. Without one it returns unavailable, never a pass. Install via elan.

  • cert_verify and residency_check delegate to signoff-cert and kvleak. Absent, they report unavailable with the pip install line — they never fake a verdict.

  • The axiom allowlist is a policy choice, not a law. Classical.choice is permitted by default; tighten it with the allowed argument if your development is constructive.

  • gridlock_check reasons about the graph you hand it. It cannot know whether that graph faithfully models your system, which is the part only you can supply.

  • No auto-repair loop is included. The server returns the compiler error; the retry is the agent's to run. An earlier draft of this README promised a bounded repair loop, which the code does not implement — the error trace is what ships.

  • No SDK, by design. MCP is JSON-RPC 2.0 over stdio; implementing it directly keeps the dependency count at zero and the whole transport auditable in one short file.

The commercial edition

This server verifies and reports. It does not gate.

The gate corpus, the automated repair mechanisms, and the certificate-issuing faucet are the licensed offering — an operator who wants a failed check to block a deploy is performing the step this package deliberately does not. See CLAIMS-MAP.md for exactly where that line sits.

Reading is free. Enforcing is licensed.

Licence

Apache-2.0 · CLEAN — exposes a toolchain and reports; implements no filed apparatus.

Honest scope — what a passing run proves, and what it does not

The two halves are inseparable. A tool that states only the first half is marketing.

It proves:

  • whether Lean source compiles, and what axioms a theorem actually rests on (including sorryAx)

  • whether a wait-for graph can wedge, and an exact k-of-n bound

  • explicitly, when a check COULD NOT RUN — unavailable is never merged into ok

It does NOT prove:

  • that a theorem says what its name or docstring suggests. #print axioms proves the dependency set is clean, never that the statement is the one you wanted

  • that a passing lake build means anything — a development full of sorry compiles and exits 0

  • anything when the toolchain is absent; it reports unavailable and stops

Full CLI reference, generated from --help: docs/CLI.md

Contributing

Bug reports and pull requests welcome — see CONTRIBUTING.md.

A false accusation is a defect of equal severity to a missed detection. If this tool flags something correct, open an issue with the input and the verdict you expected: over-refusal trains people to bypass refusals, which destroys the tool.

Citation metadata is in CITATION.cff.


The rest of the portfolio

24 artifacts, one idea: a measurement you cannot check is a press release. Every tool here reports; none of them gates.

Tools

abstain-bench

how often does a verifier pass input it could not check?

evidence

run the whole portfolio over your repo — the weakest leg, never the mean

floorgen

what must your system remember? an exact lower bound

formal-proof-mcp

a proof kernel for your coding agent ← you are here

gatecount

exactly how many states does removing this check admit?

gridlock

certify a wait-for relation cannot wedge

honestbench

measure your CI's escape rate

kvleak

cross-tenant leak scanner

kvprobe

model-substitution detector with a measured FPR

preregister

refuses to seal a plan whose conclusion is already fixed

proof-carrying-ci

the whole portfolio as one CI check, with SARIF

proof-to-code-drift

fail the build when the proof stops matching

sf-verify

re-derive admission decisions offline

signoff-cert

certificates that carry their own false-pass bound

tokencount

a token count both parties can recompute

Benchmarks — each recomputes one of our own published numbers from its certificate

illusion-bench

how many broken kernels does your oracle admit?

kv-reuse-econ-bench

recompute our economics headline

llm-tenant-isolation-bench

recompute our isolation figures

Datasets

abstain-corpus

32 inputs a verifier must NOT pass

kv-reuse-econ-traces

per-workload reuse accounting + the closed form

kv-tenant-isolation-bench

isolation observations, uninterpretable rows included

llm-precision-fingerprints

precision-labelled logprobs with a negative control

Try it in a browser — no install, no GPU

tenant-leak-demo

the residency calculator

wait-for-visualiser

paste a wait-for graph, see the cycle

Documentation

Everything above, explained in one place: https://nickharris808.github.io/evidence-docs/ — the tutorial, what this proves and what it does not, and a CLI reference generated by running --help on every published command.

The commercial edition

Everything above is measure-only and Apache-2.0: it tells you what is true and never acts on it. The enforcement side — binding a partition key at the admission decision, the compiled gate corpus, and the certificate-issuing faucet — is covered by filed patents and licensed separately.

Reading is free. Enforcing is licensed.

Verify this in ten minutes

1. Install the version that exists today

pip install "git+https://github.com/nickharris808/formal-proof-mcp@v0.1.0"

not on PyPI; the git tag is pinned so a reader installs the exact code this README documents.

2. Run one command

formal-proof-mcp --selftest

Prints the proof kernel answering, and the axiom audit catching a claim that proves nothing.

3. Where the numbers come from

Numbers in this README carry paths like results/data/.... Those receipts live in a private research monorepo and you cannot open them — they are cited so you can see exactly what was measured and where, not because the link resolves. What is public, and what you can check yourself, is: this package's own tests and --selftest; the benchmarks, which recompute the headline numbers from published inputs; and the Hugging Face datasets, whose every row names the certificate it came from. If a number here matters to you and none of those covers it, treat it as unverified.

4. What a proof here does and does not buy you

A machine-checked proof is not evidence that the thing proved means anything. This lane's own theorem-transfer engine emits an instance describing a domain that does not exist, and the Lean kernel accepts it clean; a sibling lane reached the same conclusion from the other side with theorem t : True := trivial, which is axiom-clean and proves nothing. Kernel-checking tells you a derivation is sound. Whether the statement models your system is a question no kernel answers, and it is the question worth asking.


Version 0.1.0 in the source tree · Apache-2.0 · cite via CITATION.cff in this repository · this block is generated by oss/tools/gen_readme_standard.py from a measurement of PyPI, the git tags and this tree, and --check fails if anyone edits it by hand.

Available Tools

10 tools
axiom_auditA

Audit #print axioms output against an allowlist. This is the check that catches sorryAx — a development can compile cleanly and still be full of holes, because Lean accepts sorry and exits 0.

ParametersJSON Schema
NameRequiredDescriptionDefault
outputYesraw `#print axioms` output
allowedNo

TDQS

A3.5/5.0
Behavior3/5

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

No annotations exist, so the description carries the burden. It reveals that the tool compares `#print axioms` output against an allowlist and that it is designed to catch `sorryAx`. It does not disclose behavior on mismatch, effect (read-only vs write), or handling of the optional `allowed` parameter.

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?

Two sentences, front-loaded with the core action, and the second sentence provides valuable motivation without excessive detail. Every sentence earns its place.

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 description is sufficient to understand the tool's overall purpose but is incomplete for invoking it correctly: the `allowed` parameter is never precisely defined, and there is no information about return values or failure signaling. For a two-parameter tool with no annotations or output schema, more detail is expected.

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?

The description adds the 'allowlist' concept, which maps to the `allowed` parameter that lacks a schema description, but it doesn't specify the expected string format or how violations are reported. The `output` parameter is already described in the schema, so the description adds little there. With 50% schema coverage, the description only partially compensates.

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 action ('Audit `#print axioms` output against an allowlist') and ties it to a concrete failure mode (`sorryAx`), making the tool's role clear. It does not explicitly compare with siblings like lean_check or evidence_audit, so it doesn't fully earn the top score.

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?

It provides context for when this check matters (a clean compile with `sorry` exits 0), implying use when you need to ensure no `sorry` axioms appear. It does not name alternative tools or state when not to use it, leaving the decision partially to inference.

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

boundB

What a k-of-n record actually supports, as an exact one-sided Clopper-Pearson bound. 'It passed every time' is not a bound.

ParametersJSON Schema
NameRequiredDescriptionDefault
kNoobserved failures
nYestrials
confidenceNo

TDQS

B3.1/5.0
Behavior3/5

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

With no annotations, the description carries the burden of behavioral disclosure. It clearly states the exact one-sided Clopper-Pearson method and warns that k=0 is not a bound. However, it does not disclose whether the bound is lower or upper, how missing k is handled, or what edge-case behavior occurs, so transparency is incomplete.

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?

Two sentences with no redundant material, and the core statistical method is prominent. The phrasing is slightly indirect rather than a direct 'Computes...' command, but it is appropriately sized and memorable.

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?

For a tool with no annotations and no output schema, the description is too sparse operationally. It omits the direction of the bound, the default/behavior when k is omitted (only n is required), and any parameter validation or return-shape information. The statistical essence is present, but an agent cannot confidently invoke it correctly in all intended cases.

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?

The schema already labels k as observed failures, n as trials, and confidence with a default. The description adds useful 'one-sided' and 'k-of-n' context and clarifies that a perfect record is not a bound. It does not explain k's optionality/default or confidence range, so it remains around the baseline.

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 specifies that the tool computes an exact one-sided Clopper-Pearson bound for a k-of-n record, which is a concrete and unambiguous purpose. The added warning that 'It passed every time' is not a bound reinforces the tool's role. It does not use an explicit imperative verb or name a sibling, so it misses the top score.

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?

No guidance is given about when to choose this tool over the sibling tools or about prerequisites. The only hint is a conceptual caveat about perfect records, not a selection criterion. An agent would have to infer usage from the statistical terminology.

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

cert_verifyC

Verify a signoff-cert/v1 certificate: digests, gate consistency, and the false-pass bound RECOMPUTED from the evidence. Requires signoff-cert.

ParametersJSON Schema
NameRequiredDescriptionDefault
hmac_keyNo
certificateYes
allow_unauthenticatedNo

TDQS

C2.7/5.0
Behavior2/5

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

With no annotations to fall back on, the description carries the full burden of explaining side effects, permissions, and failure modes. It mentions internal computations (digests, gate consistency, false-pass bound) but does not disclose what the tool does beyond that—no mention of errors, required access, or consequences of verification failure.

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 extremely concise—two sentences—and immediately states the primary action and key verification aspects. It is well-structured, with the action first and the required capability noted at the end, fitting comfortably within a short description.

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?

The description lacks critical context: no output format or return values are described (no output schema exists), no error conditions are mentioned, and the tool's role relative to sibling tools is not clarified. Given the complexity of the certificate verification process, this is insufficient for an agent to know what to expect.

Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.

Parameters1/5

Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?

The input schema has zero parameter descriptions, and the tool description does not compensate. While 'certificate' is implied by the resource name, there is no explanation of `hmac_key` or `allow_unauthenticated`. This leaves agents without enough information to construct correct arguments.

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 clearly states the core action ('Verify a signoff-cert/v1 certificate') and lists specific checks (digests, gate consistency, false-pass bound recomputation). It is clear enough to distinguish the tool's primary function from generic 'check' or 'audit' tools, though it does not explicitly name sibling alternatives.

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 description provides no explicit guidance on when to use this tool versus the sibling tools. The only contextual hint is 'Requires `signoff-cert`', which suggests a prerequisite but does not clarify when this verification is appropriate or when another tool should be chosen.

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

evidence_auditA

Run every applicable verifier over a directory and aggregate to ONE verdict -- the weakest leg, never the mean. Requires evidence.

ParametersJSON Schema
NameRequiredDescriptionDefault
pathNodirectory to audit

TDQS

A3.8/5.0
Behavior3/5

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

With no annotations provided, the description carries the full burden of behavioral disclosure. It does reveal a meaningful non-obvious behavior: the verdict is the weakest leg, never the mean, and a prerequisite ('Requires `evidence`') exists. However, it leaves important traits undisclosed, such as what constitutes 'evidence', what the verdict format is, whether the operation is read-only, and how failures are handled.

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 two sentences with no filler. The core purpose and unique aggregation rule are front-loaded, and every clause contributes meaningful information, even if one clause is cryptically worded.

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?

This is an orchestrating tool that runs multiple verifiers and produces a verdict, yet there is no output schema and no annotation. The description does not define what a 'verdict' looks like, what 'every applicable verifier' means in concrete terms, what 'Requires `evidence`' refers to, or what happens if the path is invalid or the evidence is missing. Given the complexity, the description leaves too much for the agent to infer.

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?

The schema already documents the single parameter `path` as 'directory to audit', so schema description coverage is 100%. The description adds the 'Requires `evidence`' constraint, which could plausibly tell the agent what must be inside `path`, but it is too ambiguous to clearly enhance parameter understanding. Baseline 3 is appropriate.

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 uses a specific verb ('Run') and a clear resource ('every applicable verifier over a directory'), then adds a precise aggregation rule ('ONE verdict -- the weakest leg, never the mean'). This strongly distinguishes it from sibling tools like lean_check or cert_verify, which appear to be individual verifiers rather than the aggregate audit.

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 description makes the use case clear: call this tool when you want every applicable verifier run and combined into a single verdict. It does not explicitly name alternatives or state when not to use it, but the 'every applicable verifier' phrasing implicitly contrasts with the individual sibling tools. The 'Requires `evidence`' constraint gives some prerequisite context, though it is ambiguous.

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

gate_countA

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.

ParametersJSON 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

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.

gridlock_checkA

Certify that a wait-for relation cannot wedge. Returns the actual cycle when one exists. Supply ranks to also check strict decrease, which is what bounds progress — acyclicity alone only forbids a cycle.

ParametersJSON Schema
NameRequiredDescriptionDefault
edgesYes[[waiter, holder], ...]
ranksNo

TDQS

A3.8/5.0
Behavior4/5

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

With no annotations provided, the description carries the behavioral disclosure burden and does reasonably well: it explains the core certification, the cycle-returning behavior, and the semantic role of ranks in proving progress. It still does not state what happens when no cycle exists or whether the operation is side-effect free, but the disclosed behavior is meaningful and non-tautological.

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 concise, front-loaded, and every sentence contributes: purpose, normal return behavior, and optional parameter semantics. There is no filler or repetition.

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 description covers the core purpose and the optional ranks behavior well, but because there is no output schema, it should clarify what the tool returns when no cycle exists and how successful certification is represented. The ranks object format is also left vague, though the parameter is optional.

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?

The schema describes edges as '[[waiter, holder], ...]', and the description adds the wait-for relation context. It also explains that ranks are used to verify strict decrease, giving semantic meaning to an otherwise undocumented object parameter, although the exact shape of the ranks object remains underspecified.

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 clearly identifies a specific operation — certifying that a wait-for relation cannot wedge — and explains that it returns the actual cycle when one exists. It is distinct in substance from the sibling tools, though it does not explicitly name any alternative for comparison.

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 description gives useful contextual guidance: supply ranks to check strict decrease, and notes that acyclicity alone is insufficient for bounded progress. However, it does not explicitly state when to use this tool versus the sibling verification tools or when to prefer another check.

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

lean_checkA

Compile a Lean 4 snippet and return the compiler's verdict. On failure the real error is returned so the agent can repair its own proof. If no Lean toolchain is installed the result is unavailable — never a pass.

ParametersJSON Schema
NameRequiredDescriptionDefault
sourceYesLean 4 source
timeoutNo

TDQS

A4.4/5.0
Behavior5/5

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

No annotations are provided, so the description carries the full burden. It discloses that failures return the real error, and that a missing toolchain results in 'unavailable' rather than a pass, giving an honest account of likely outcomes.

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 sentences, direct, and free of unnecessary detail. It front-loads the core purpose and then adds important edge-case behavior efficiently.

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?

The description covers the main purpose and failure modes, which is helpful given there is no output schema. However, it does not describe the success response format or timeout behavior, leaving some context incomplete.

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?

The schema already describes 'source' as 'Lean 4 source', and the description's 'snippet' adds little. The 'timeout' parameter has no semantic explanation (e.g., units or default behavior), so the description does not fully compensate for the schema gap.

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 clearly states the tool compiles a Lean 4 snippet and returns the compiler's verdict, using a specific verb ('compile') and a specific resource ('Lean 4 snippet'). It also distinguishes the tool's behavior in failure and environment-missing cases.

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 description gives clear context for when the tool is appropriate—when a Lean 4 snippet needs checking—and explains failure is repairable. It does not explicitly compare with sibling tools or state when not to use it, so it falls short of a perfect score.

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

prereg_checkA

Before running an experiment, check that its decision rule CAN come out both ways. Returns UNFALSIFIABLE when the finding -- or the null -- can never fire over the declared metric supports. Requires preregister.

ParametersJSON Schema
NameRequiredDescriptionDefault
metricsYeseach metric to its support: a list of values, or {lo, hi} (add "type": "integer" for integers)
decision_ruleYese.g. `auc > 0.7 and n_probes >= 30`

TDQS

A4.1/5.0
Behavior4/5

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

With no annotations, the description carries the burden and actually discloses a concrete behavior: returns UNFALSIFIABLE when the finding or null can never fire over declared supports, and requires preregister. It does not state the return value when the rule is falsifiable, which is a minor gap.

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?

Three short sentences, each earning its place: when to use, what it returns, and the dependency. No filler or repetition.

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?

Parameters are fully covered by the schema, but there is no output schema and no annotations, so the description should define the full return contract. It details only the UNFALSIFIABLE case and leaves the falsifiable outcome implicit, which is a meaningful gap for an agent.

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 100%, so the schema already documents decision_rule and metrics. The description only adds the term 'declared metric supports' and does not go beyond the schema, so baseline 3 is appropriate.

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 specific verb ('check') and resource ('decision rule') and describes the falsifiability criterion ('CAN come out both ways'). The UNFALSIFIABLE return and prerequisite set it apart from the sibling check/audit tools.

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?

Explicitly says 'Before running an experiment', giving clear temporal context for when to call it. It does not name alternatives or exclusions, but the context plus the distinct UNFALSIFIABLE outcome makes the intended use reasonably clear.

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

residency_checkB

Can a cross-tenant cache probe on this model even be interpreted? Returns failed when the victim's state could not have stayed resident, because a null from an evicted cache is not an all-clear. Requires kvleak.

ParametersJSON Schema
NameRequiredDescriptionDefault
modelYes
n_prefixesNo
tokens_eachNo
kv_budget_gibYes

TDQS

B3.3/5.0
Behavior4/5

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

With no annotations provided, the description carries the full responsibility for behavioral disclosure. It explains an important semantic subtlety: a null result from an evicted cache is not an all-clear, and it defines what `failed` means. It does not mention side effects, permissions, or other possible return states, but the key interpretability trap is clearly surfaced.

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 compact, with two sentences that each add value: one defines the core question and failure semantics, and the other names the required dependency. The rhetorical question is slightly less direct than an explicit imperative, but the description remains tightly structured and free of filler.

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?

For a four-parameter tool with no annotations and no output schema, the description is incomplete: it explains the failure case but not what a successful or interpretable outcome looks like, nor what the parameters mean. It provides purpose, one dependency, and one important semantic caveat, but that is not enough for an agent to invoke the tool correctly with confidence.

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%, so the description must compensate for the lack of parameter documentation, but it does not explain `model`, `kv_budget_gib`, `n_prefixes`, or `tokens_each`. The cache-probe context hints at the role of `kv_budget_gib`, but an agent would struggle to know what values to supply for the two required parameters and how the optional parameters affect the check.

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 clearly identifies the tool as a check on whether a cross-tenant cache probe result can be interpreted, and it specifies a concrete output condition: `failed` when the victim's state could not have stayed resident. It is not a bare tautology and conveys a distinct domain purpose. However, it is phrased as a question rather than a direct verb phrase and does not distinguish itself from sibling tools like `lean_check` 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 Guidelines3/5

Does the description explain when to use this tool, when not to, or what alternatives exist?

The description gives one operational prerequisite, `Requires kvleak`, which tells the agent that this dependency must be available before calling. The intended use case is implied: use it when you need to know whether a cross-tenant cache probe's result is interpretable given residency. It does not explicitly state when to prefer this over alternatives or when not to use it.

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

state_floorC

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.

ParametersJSON 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

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.

Tool Schema Changelog

Recent tool additions, removals, and schema changes observed during successful MCP inspections.

  1. 10 tool updatesv0.1.0
    • First observedaxiom_audit
    • First observedbound
    • First observedcert_verify
    • First observedevidence_audit
    • First observedgate_count
    • First observedgridlock_check
    • First observedlean_check
    • First observedprereg_check
    • First observedresidency_check
    • First observedstate_floor

TDQS

A3.6/5.0

Scored across 10 tools

Disambiguation5/5

Each tool targets a distinct verification or counting task—Lean compilation, axiom auditing, bounds, deadlock detection, certificate verification, residency interpretation, preregistration falsifiability, state floors, gate impact, and evidence aggregation. Even the closest pair, state_floor and gate_count, is clearly separated by what each counts.

Naming Consistency4/5

Most tools follow a descriptive object_action pattern such as lean_check, gridlock_check, prereg_check, and cert_verify, and all names use lower-case snake_case. However, bound, state_floor, and gate_count are noun-phrase names rather than action-phrase names, so the convention is not perfectly uniform.

Tool Count5/5

Ten tools is within the ideal 3-15 range, and each tool earns its place by covering a distinct aspect of formal proof and evidence verification. The count feels well-scoped for a server spanning Lean checking, axiom auditing, and specialized domain proofs.

Completeness4/5

The set covers the main verification lifecycle well: compilation, axiom auditing, certificate verification, evidence aggregation, and several specialty proof checks. The primary gap is the lack of a general proof-construction or proof-search tool, and several tools require external packages, making the surface strong but not fully self-contained.

Maintenance

ActivityMaintained
ResponsivenessNo issues

Resources

Unclaimed servers have limited discoverability.

Looking for Admin?

If you are the server author, to access and configure the admin panel.

Related MCP Connectors

Related MCP Servers

  • A
    license
    Not graded
    quality
    C
    maintenance
    An MCP server that provides fact-checking capabilities and truth anchoring for AI agents using verified data sources.
    MIT
  • A
    license
    B
    quality
    B
    maintenance
    An MCP server that enforces fail-closed deterministic checks, independent refute-first review, and tamper-evident hash-chained receipts for AI agent outputs before claiming completion.
    4
    3
    MIT
  • A
    license
    A
    quality
    A
    maintenance
    An MCP server that provides tools for certificate verification, equivalence proving, and pre-registration sealing, enabling AI agents to re-derive verdicts from artifacts rather than trust assertions.
    9
    Apache 2.0