Skip to main content
Glama
Sign In
OrangePro MCP

OrangePro MCP

Official
by OrangeproAI
OverviewSchemaSourceRelated ServersDiscussionsAdmin
TypeScript
Local

Run dynamic targeted proof

orangepro_prove

Runs a targeted mutation proof for a CodeSymbol, verifies baseline tests pass and a sentinel mutation fails the same test at an assertion, then appends a metadata-only ledger certificate.

Instructions

Run the dynamic targeted-proof oracle for a CodeSymbol and append a metadata-only ledger certificate. Public Proven closes only when baseline green plus a valid sentinel mutation of the credited symbol fails the same test at an assertion. Static record_run is diagnostics only.

Input Schema

NameRequiredDescriptionDefault
methodNoOptional consistency check. If provided, must match the member derived from target_symbol.
run_idNoOptional caller-supplied run id. Defaults to a local monotonic id.
runnerNoTest runner override. Default auto.
sourceNoSource checkout containing the test and target files. Defaults to workspace.
test_envNoExplicit non-secret KEY=value env entries for the test run.
test_runNoGo: fully-anchored test name for `go test -run`, e.g. '^TestCompute$' (required for Go targets). Java: 'TestClass#testMethod', e.g. 'CalculatorTest#addsTwoNumbers' (required for Java targets).
target_idNoOptional graph target id that must resolve to exactly one hard-linked CodeSymbol.
test_pathNoTS/JS: repo-relative test file to run (required for TS/JS targets).
workspaceNoLocal workspace root. Defaults to the current directory.
timeout_msNoPer baseline/mutant test timeout.
jest_configNoRepo-relative Jest config path.
replacementNoTS/JS: inert sentinel body, e.g. 'return null;' or 'return {"ok":false};'. Must be JSON-only per the oracle (required for TS/JS targets). Go derives its own sentinel.
target_fileNoOptional consistency check. If provided, must match the file derived from target_symbol.
target_symbolNoExact CodeSymbol external id, e.g. sym:src/service.ts#OrderService.createOrder. Preferred.
vitest_configNoRepo-relative Vitest config path.
replacement_modeNoSentinel wrapping mode. Default return-json.
link_node_modulesNoTrusted-repo speed mode: symlink node_modules into temp copies.

Schema Changelog

Changes observed during successful MCP inspections.

  1. Changed1 schema field changed
    • removedInput schema / additionalProperties
      Removed value: -false
  2. Addedv0.2.59

TDQS

A3.6/5.0
Behavior4/5

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

Annotations already declare non-read-only, non-idempotent, open-world, and non-destructive behavior. The description adds useful behavioral context beyond those hints: it appends a metadata-only ledger certificate, and it specifies the success condition involving baseline green plus a sentinel mutation failing at an assertion. It does not describe response shape or failure modes in detail.

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 dense sentences and is reasonably front-loaded with the core action. Every sentence contributes to purpose, success condition, or sibling contrast, though the jargon-heavy phrasing could be clearer for an agent.

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?

For a complex 17-parameter tool with no output schema, the description explains the conceptual proof procedure and the ledger-certificate side effect. However, it does not explain what the tool returns, how failures are reported, or which runner-specific inputs are required, leaving important invocation context to the schema alone.

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%, so all 17 parameters are already documented in the input schema. The description mentions the CodeSymbol target concept but does not add syntax, format, or per-runner parameter guidance beyond what the schema provides. Baseline 3 is appropriate when the schema does the heavy lifting.

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 verb and resource: running the dynamic targeted-proof oracle for a CodeSymbol and appending a metadata-only ledger certificate. It distinguishes itself from the sibling orangepro_record_run by labeling that tool as diagnostics only. The domain jargon is dense but specific, not tautological.

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 implies when this tool is appropriate by explaining that Public Proven requires a baseline green plus a valid sentinel mutation, and it contrasts static record_run as diagnostics only. However, it does not explicitly say when to use this versus orangepro_prove_loop or other verification-related siblings, and it gives no explicit exclusions.

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

Deploy Server

Other Tools