Skip to main content
Glama
nickharris808

formal-proof-mcp

evidence_audit

Audit a directory with all applicable verifiers, then aggregate outcomes to one verdict—the weakest leg, never the mean. Requires evidence.

Instructions

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

Input Schema

TableJSON Schema
NameRequiredDescriptionDefault
pathNodirectory to audit

Schema Changelog

Changes observed during successful MCP inspections.

  1. First observedv0.1.0

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.