kernel_check_proof

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

With no annotations provided, the description fully discloses behavior: it runs locally, exit code 0 means accepted, else proof is wrong, requires lean binary, and overridable via environment variable. It also describes the return format including fields like accepted, exit_code, etc.

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 and well-structured: purpose first, then trust significance, exit code meaning, prerequisites, and return format. Every sentence adds value without redundancy.

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 tool has one parameter and an output schema. The description covers prerequisites, error handling (non-zero exit), return fields, and even an environment variable override. It is fully complete for a tool of this complexity.

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 single parameter lean_source has 0% schema description coverage, but its name and title are self-explanatory. The description mentions 'proof string' in the first line, giving context. A direct parameter description would improve clarity, but it is still adequate.

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 'Run the Lean 4 kernel on a proof string locally', specifying the verb, resource, and scope. It distinguishes from siblings like download_lean_proof (download) and verify_reasoning (other verification) by emphasizing it is the trust anchor and runs locally.

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 explains the exit code meaning and the requirement for the lean binary, including installation via elan. While it doesn't explicitly contrast with siblings, the context of being the trust anchor implies when to use this tool for final kernel verification.

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