formal-proof-mcp
Click on "Install Server".
Wait a few minutes for the server to deploy. Once ready, it will show a "Started" state.
In the chat, type
@followed by the MCP server name and your instructions, e.g., "@formal-proof-mcpCheck theorem.lean for Lean errors"
That's it! The server will respond to your query, and you can continue using it as needed.
Here is a step-by-step guide with screenshots.
formal-proof-mcp
Your agent says it proved the theorem. Did anything actually check?
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 |
| the check ran and passed |
| the check ran and failed — with the real error attached, for the repair loop |
| 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-mcpis 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 dependenciescert_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 stdioWire it into Claude Desktop or Cursor:
{
"mcpServers": {
"formal-proof": { "command": "formal-proof-mcp" }
}
}The ten tools
tool | what it answers |
| Does this Lean 4 source compile? On failure, returns the compiler's own error so the agent repairs its proof instead of asserting one. |
| What does the theorem actually rest on? Catches |
| What does a k-of-n record support? Exact one-sided Clopper–Pearson. "It passed every time" is not a bound. |
| Can this wait-for relation wedge? Returns the actual cycle, and optionally checks a strictly decreasing rank. |
| Is this |
| 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 |
| can this experiment's decision rule come out both ways? |
|
| how many states must the system distinguish? |
|
| exactly how many states does removing this check admit? |
|
| run every applicable verifier over a tree, aggregate to one verdict |
|
Not yet on PyPI.
pip install formal-proof-mcpis 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-runnerevidence-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-mcpinitialize -> {'name': 'formal-proof-mcp', 'version': '0.1.0'} 2024-11-05
id=2 isError=True status=failed wait-for cycle: a -> b -> c -> aAnd 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 compilesisError 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_checkneeds a Lean toolchain. Without one it returnsunavailable, never a pass. Install via elan.cert_verifyandresidency_checkdelegate tosignoff-certandkvleak. Absent, they reportunavailablewith thepip installline — they never fake a verdict.The axiom allowlist is a policy choice, not a law.
Classical.choiceis permitted by default; tighten it with theallowedargument if your development is constructive.gridlock_checkreasons 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 —
unavailableis never merged intook
It does NOT prove:
that a theorem says what its name or docstring suggests.
#print axiomsproves the dependency set is clean, never that the statement is the one you wantedthat a passing
lake buildmeans anything — a development full ofsorrycompiles and exits 0anything when the toolchain is absent; it reports
unavailableand 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
how often does a verifier pass input it could not check? | |
run the whole portfolio over your repo — the weakest leg, never the mean | |
what must your system remember? an exact lower bound | |
a proof kernel for your coding agent ← you are here | |
exactly how many states does removing this check admit? | |
certify a wait-for relation cannot wedge | |
measure your CI's escape rate | |
cross-tenant leak scanner | |
model-substitution detector with a measured FPR | |
refuses to seal a plan whose conclusion is already fixed | |
the whole portfolio as one CI check, with SARIF | |
fail the build when the proof stops matching | |
re-derive admission decisions offline | |
certificates that carry their own false-pass bound | |
a token count both parties can recompute |
Benchmarks — each recomputes one of our own published numbers from its certificate
how many broken kernels does your oracle admit? | |
recompute our economics headline | |
recompute our isolation figures |
Datasets
32 inputs a verifier must NOT pass | |
per-workload reuse accounting + the closed form | |
isolation observations, uninterpretable rows included | |
precision-labelled logprobs with a negative control |
Try it in a browser — no install, no GPU
the residency calculator | |
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 --selftestPrints 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 toolsaxiom_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.
| Name | Required | Description | Default |
|---|---|---|---|
| output | Yes | raw `#print axioms` output | |
| allowed | No |
TDQS
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.
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.
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.
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.
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.
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.
| Name | Required | Description | Default |
|---|---|---|---|
| k | No | observed failures | |
| n | Yes | trials | |
| confidence | No |
TDQS
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.
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.
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.
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.
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.
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.
| Name | Required | Description | Default |
|---|---|---|---|
| hmac_key | No | ||
| certificate | Yes | ||
| allow_unauthenticated | No |
TDQS
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.
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.
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.
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.
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.
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.
| Name | Required | Description | Default |
|---|---|---|---|
| path | No | directory to audit |
TDQS
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.
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.
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.
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.
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.
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.
| Name | Required | Description | Default |
|---|---|---|---|
| domain | Yes | each variable to a list of values or {lo, hi[, step]} | |
| policy | Yes | the full policy, with the check | |
| weakened | Yes | the policy with the check removed |
TDQS
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.
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.
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.
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.
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.
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.
| Name | Required | Description | Default |
|---|---|---|---|
| edges | Yes | [[waiter, holder], ...] | |
| ranks | No |
TDQS
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.
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.
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.
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.
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.
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.
| Name | Required | Description | Default |
|---|---|---|---|
| source | Yes | Lean 4 source | |
| timeout | No |
TDQS
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.
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.
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.
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.
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.
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.
| Name | Required | Description | Default |
|---|---|---|---|
| metrics | Yes | each metric to its support: a list of values, or {lo, hi} (add "type": "integer" for integers) | |
| decision_rule | Yes | e.g. `auc > 0.7 and n_probes >= 30` |
TDQS
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.
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.
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.
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.
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.
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.
| Name | Required | Description | Default |
|---|---|---|---|
| model | Yes | ||
| n_prefixes | No | ||
| tokens_each | No | ||
| kv_budget_gib | Yes |
TDQS
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.
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.
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.
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.
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.
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.
| Name | Required | Description | Default |
|---|---|---|---|
| answers | Yes | rows of {when: {...}, answer: ...} | |
| default | No | answer for unmatched situations | |
| variables | Yes | each variable to its finite domain (a list) | |
| has_default | No | ||
| budget_states | No | if given, also test this budget for impossibility |
TDQS
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.
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.
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.
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.
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.
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.
10 tool updates
v0.1.0- First observed
axiom_audit - First observed
bound - First observed
cert_verify - First observed
evidence_audit - First observed
gate_count - First observed
gridlock_check - First observed
lean_check - First observed
prereg_check - First observed
residency_check - First observed
state_floor
TDQS
Scored across 10 tools
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.
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.
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.
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
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
Trust checks for MCP servers: trust scores, tool-drift detection, signed diligence receipts. Free.
Hosted MCP server for AI agent identity, permissions, verification, and reusable proof.
1Independent trust scores, tool surfaces and change history for MCP servers.
The MCP server that vets MCP servers: identity, risk grade and per-tool risk before you install.
Related MCP Servers
- AlicenseNot gradedqualityCmaintenanceAn MCP server that provides fact-checking capabilities and truth anchoring for AI agents using verified data sources.MIT
- AlicenseAqualityDmaintenanceAn MCP server that exposes the Prova reasoning verifier, enabling AI agents to verify their own reasoning and kernel-check Lean 4 proofs before outputting answers.5MIT
- AlicenseBqualityBmaintenanceAn 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.43MIT
- AlicenseAqualityAmaintenanceAn 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.9Apache 2.0